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

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Wed Mar 19 12:41:22 CET 2014


Hi Alan,

> but when
> I add the fact that it is a permutation, I no longer can prove the
> sorting (yet can prove the permutation part).

This is a known behavior of SMT solvers that, when you add stuff to the
logical context, you may loose proofs. (More terms means more lemmas
that are triggered means more work to do means potential timeout.)

Anyway, I was able to prove you example (using Why3 0.83), including the
permutation property, but using at least two SMT solvers, as Claudio did.

> 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?

So, there is no such theory/module. But you are free to make your own,
and even to contribute tou our library in such a way.

This should resembles the theory map.Occ, that is

	function maximum (map int int) int int : int
	  (** maximum value in m[l..u[ *)

 	axiom max_one: forall m l. maximum m l (l+1) = m[l]

	axiom max_left: forall m l u. l+1 < u ->
	  maximum m l u = max m[l] (maximum m (l+1) u)

(or, equivalently, starting from the right), together with suitable
lemmas if needed (such as transitivity, but be careful of non-emptiness).

-- 
Jean-Christophe



More information about the Why3-club mailing list