[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