[Why3-club] additional invariants cause proven ones to fail?

Alan Schmitt alan.schmitt at polytechnique.org
Tue Mar 18 19:15:54 CET 2014


I'm playing with a variation of bubble sort where instead of returning
a boolean indicating whether a swap occurred, the algorithm returns the
index of the last swap (so that the next round of bubbling ends earlier
in the array). I'm able to prove that the sorting is correct, but when
I add the fact that it is a permutation, I no longer can prove the
sorting (yet can prove the permutation part).

Attached is the corresponding file, with the permutation postcondition
commented out. This is proven with alt-ergo 0.95.2 and why3 0.82 (the
current version on opam). If I remove the comments (to additionally
prove permutation), the sorting proof fails.

Is this a bug? Do you see the same behavior?

While I'm at it, a crucial invariant I had to use was the following one:
#+begin_src why3
    ensures  { forall v:int. (forall k:int. s <= k < e -> (old a)[k] <= v) 
                          -> (forall k:int. s <= k < e -> a[k] <= v) }

I searched for properties of maxima on arrays but could not find
anything. Is there such a theory/module? (I often have to add such
properties because they are usually not deduced from the fact that the
new array is a permutation of the old one.)



-------------- next part --------------
A non-text attachment was scrubbed...
Name: bubble.mlw
Type: application/octet-stream
Size: 1641 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20140318/7035818a/attachment.obj>

More information about the Why3-club mailing list