[Why3-club] Working with loop invariants

Kruer, Joseph C. jkruer at draper.com
Wed Jul 11 23:02:48 CEST 2018

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.

More information about the Why3-club mailing list