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

Cláudio Amaral coa at dcc.fc.up.pt
Wed Mar 19 11:29:39 CET 2014

I have tried your file.

the VC for onebubble was not proven right away and neither the more
complete VC for bubble

splitting the VCs (why3ide split button) I was able to prove everything
automatically with my setup (needed a combination of alt-ergo 0.95.1 and Z3
3.2, funny that it worked better than 4.1)

I believe that by having the VC all in one formula makes it harder for the
provers. If sub-VCs are not related the search space can de reduced and the
provers focus on one disjoint matter at a time.

Someone with more experience might give a better explanation


On Tue, Mar 18, 2014 at 6:15 PM, Alan Schmitt <
alan.schmitt at polytechnique.org> wrote:

> Hello,
> 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) }
> #+end_src
> 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.)
> Thanks,
> Alan
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20140319/69eb0461/attachment.html>

More information about the Why3-club mailing list