So, I create a bunch of Alloy signatures, predicates, and facts. I express a lot of relationships. I write in English some statements representing the Alloy model:
A is a ...
B is ...
Then I create an Alloy assertion. No counterexamples found. What is the appropriate English statement for the assertion? I believe the assertion represents a conclusion:
A is a ...
B is ...
Therefore, ...
Do you agree? Does an Alloy assertion with no counterexample represent a conclusion ("therefore" statement)?
There's two points that would discourage me to call an assertion, for which counterexamples where not found, "conclusion":
- The fact that no counter-examples have been found is to put in perspective with the fact that the search for counterexamples has been performed on a limited scope. In general, I would say that the lack of counterexamples doesn't really prove anything out of the scope it is performed in. At most it might give a certain degree of confidence that the assertion could indeed hold as well in a broader scope.
- From you definition of conclusion, "A Therefore B". It is somehow implied that there's a logical connection between A and B, which is not always the case between facts and assertions. What if my assertion is a tautology ? Wouldn't it feel weird to claim: "I specified those facts in my model therefore 1=1" ? :-)