[Why3-club] Specifying the order in which loop invariant may be proven

David MENTRE dmentre at linux-france.org
Wed Mar 26 16:23:21 CET 2014


Hello Alan,

Le 26/03/2014 16:12, Alan Schmitt a écrit :
> And I tried "/\" and it did not ... this is
> quite a big difference between the two.

This is partially documented:
"""
Notice that there are two symbols for the conjunction: /\ and &&, and 
similarly for
disjunction. They are logically equivalent, but may be treated slightly 
differently by
some transformations. For instance, split transforms the goal A /\ B 
into subgoals A
and B, whereas it transforms A && B into subgoals A and A -> B. 
Similarly, it transforms
not (A || B) into subgoals not A and not ((not A) /\ B).
""
Why3 0.83 manual, p. 77.

I said partially because the form "invariant { I(i) && J(i) }" is new to me.

Best regards,
david




More information about the Why3-club mailing list