[Why3-club] Working with loop invariants

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Thu Jul 12 09:21:46 CEST 2018

Dear Jay,

Here are some hints:

- Wrong loop invariants may result in returns/ensures being discharged
due to a logical inconsistency in the context. In your case, when you
exit the loop you have both i=n (by the loop) and i<=n-1 (by your loop
invariant) and that explains why returns/ensures are easily discharged.

- You don't need to add a loop invariant about i in a for loop on i;
this is done automatically.

- You should not introduce an axiom saying that the length of any array
is positive. That's also introducing an inconsistency. Instead, you
should use specific requires in functions where arrays are non-empty.

- You may be interested in this example from our gallery, which is very
close to what you want to do:


Hope this helps,

On 11/07/2018 23:02, Kruer, Joseph C. wrote:
> I'm a student working with Why3 (1.0.0, with Z3 4.6.0 as my primary solver) and as a proof-of-concept I've decided to prove a simple "string sanitization" routine.
> All it does is remove all the backslashes in an input string. I have reduced what I think to be the full specification of such a function down to three properties:
> 1. The obvious one: the resultant string contains no backslashes;
> 2. Preservation of contents: the resultant string has the same varieties of and quantities thereof as the non-backslash characters of the source string;
> 3. Preservation of order: the order in which characters appear in the destination string matches that of the source string.
> I am fairly confident that I have encoded these properties accurately as Why3 predicates, and in fact I have managed to get Why3 to prove that my implementation conforms to my full spec!:
> https://lpaste.net/5659415385884065792 (Sorry if webpastes are bad etiquette; I am new to the list.)
> The problem I'm facing (marked with "FIXME" in the file linked above) now is that the loop invariants I have on my for loop won't verify. When I modify the loop invariants to correctly reflect the state at every point in the loop (namely, allowing i to range up to n and j up to n+1), my more important three properties fail to verify. I've been tweaking this for a few hours now and haven't made much headway, so I was hoping that someone could offer a novice like myself some pointers to fixing this and getting the green lights I so badly crave. On a perhaps more philosophical note, should I even worry about/bother with this issue if the properties I care about are proving?
> Thanks much,
> - Jay
> ________________________________
>  Notice: This email and any attachments may contain proprietary (Draper non-public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email.
> ________________________________
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club

More information about the Why3-club mailing list