[Why3-club] lemma visibility

Julia Lawall julia.lawall at lip6.fr
Mon Jan 28 07:22:22 CET 2019

In the following:

  val ([]<-) (a: array 'a) (i: int) (v: 'a) : unit writes {a}
    requires { [@expl:index in array bounds] 0 <= i < length a }
    ensures  { a.elts = Map.set (old a).elts i v }
    ensures  { a = (old a)[i <- v] }

a = (old a)[i <- v] implies a.elts = Map.set (old a).elts i v

So is it necessary to have both of them?  In other cases, I have found
that duplicating lemmas can increase the running time, but I don't have an
example where that is a problem here.


More information about the Why3-club mailing list