On Thu, 8 Mar 2018, Alix TRIEU wrote:
> On Thu, Mar 8, 2018 at 11:09 AM Julia Lawall <julia.law...@lip6.fr> wrote:
>
>
> On Tue, 27 Feb 2018, Claude Marché wrote:
>
> >
> > Here is another typical usage, say for the swap function:
> >
> >
> > let swap (a:array 'a) (i:int) (j:int) : unit
> > requires { 0 <= i < a.length /\ 0 <= j < a.length }
> > writes { a }
> > ensures { a[i] = (old a)[j] }
> > ensures { a[j] = (old a)[i] }
> > ensures { forall k. 0 <= k < a.length /\ k <> i /\ k <> j
> -> a[k] =
> > (old a)[k] }
> > = let v = a[i] in
> > a[i] <- a[j];
> > a[j] <- v
>
> Is it possible to use the old keyword in a loop invariant?
> Concretely, my
> code consists of a loop that doesn't touch an array at all, and
> then some
> code afterwards that may update an element. I wonder if I need
> a loop
> invariant that indicates that the array is not changed, ie
>
> invariant { chosen = (old chosen) }
>
> and if so what is the proper way to express that.
>
> thanks,
> julia
>
>
> You could put a label before the loop section, and use the at keyword in
> your invariants.
> Example taken from the gallery of verified
> programs: http://toccata.lri.fr/gallery/flag2.en.html
>
> 'Init:
> while !i < !r do
> invariant {
> forall c:color. nb_occ !a 0 n c = nb_occ (at !a 'Init) 0 n c }
> variant { !r - !i }
> match get !a !i with
> | Blue -> swap a !b !i; b := !b + 1; i := !i + 1
> | White -> i := !i + 1
> | Red -> r := !r - 1; swap a !r !i
> end
> done
>
> The invariant states that the number of occurences of the color c between
> indexes 0 and n in array !a is the same as in the array at the start of the
> loop, i.e. at the 'Init label.
That seems to be accepted. Thanks.
julia
>
> Alix
>
>
> >
> >
> >
> >
> > Le 27/02/2018 à 08:45, Guillaume Melquiond a écrit :
> > > Le 27/02/2018 à 08:18, Julia Lawall a écrit :
> > >> Is it possible to write an ensures that refers to both the
> original and
> > >> final value of an array. For exampe, if one makes a
> function update ar i
> > >> v, one might want to write an ensures that indicates that
> only the ith
> > >> element of the array is updated. All of the others remain
> unchanged.
> > >
> > > Use the "old" keyword. For example, the "ensures" clause of
> the update
> > > function in modules/array.mlw is
> > >
> > > ensures { a.elts = M.set (old a.elts) i v }
> > >
> > > Best regards,
> > >
> > > Guillaume
> > > _______________________________________________
> > > Why3-club mailing list
> > > Why3-club@lists.gforge.inria.fr
> > > https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >
> > --
> > Claude Marché | tel: +33 1 69 15 66
> 08
> > INRIA Saclay - Île-de-France |
> > Université Paris-sud, Bat. 650 |
> http://www.lri.fr/~marche/
> > F-91405 ORSAY Cedex |
> > _______________________________________________
> > Why3-club mailing list
> > Why3-club@lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >_______________________________________________
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
>
>_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
