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 ! <http://why3.lri.fr/stdlib/ref.html#prefix.20.21_22>i <
<http://why3.lri.fr/stdlib/int.html#infix.20.3C_16> !
<http://why3.lri.fr/stdlib/ref.html#prefix.20.21_22>r do
invariant {
forall c:color
<http://toccata.lri.fr/gallery/flag2.en.html#color_13>. nb_occ
<http://toccata.lri.fr/gallery/flag2.en.html#nb_occ_18> !
<http://why3.lri.fr/stdlib/ref.html#prefix.20.21_18>a 0 n c = nb_occ
<http://toccata.lri.fr/gallery/flag2.en.html#nb_occ_18> (at !
<http://why3.lri.fr/stdlib/ref.html#prefix.20.21_18>a 'Init) 0 n c }
variant { ! <http://why3.lri.fr/stdlib/ref.html#prefix.20.21_18>r
- <http://why3.lri.fr/stdlib/int.html#infix.20-_100> !
<http://why3.lri.fr/stdlib/ref.html#prefix.20.21_18>i }
match get <http://why3.lri.fr/stdlib/map.html#get_14> !
<http://why3.lri.fr/stdlib/ref.html#prefix.20.21_22>a !
<http://why3.lri.fr/stdlib/ref.html#prefix.20.21_22>i with
| Blue <http://toccata.lri.fr/gallery/flag2.en.html#Blue_13> ->
swap <http://toccata.lri.fr/gallery/flag2.en.html#swap_71> a !
<http://why3.lri.fr/stdlib/ref.html#prefix.20.21_22>b !
<http://why3.lri.fr/stdlib/ref.html#prefix.20.21_22>i; b :=
<http://why3.lri.fr/stdlib/ref.html#infix.20:.3D_24> !
<http://why3.lri.fr/stdlib/ref.html#prefix.20.21_22>b +
<http://why3.lri.fr/stdlib/int.html#infix.20.2B_86> 1; i :=
<http://why3.lri.fr/stdlib/ref.html#infix.20:.3D_24> !
<http://why3.lri.fr/stdlib/ref.html#prefix.20.21_22>i +
<http://why3.lri.fr/stdlib/int.html#infix.20.2B_86> 1
| White <http://toccata.lri.fr/gallery/flag2.en.html#White_13> ->
i := <http://why3.lri.fr/stdlib/ref.html#infix.20:.3D_24> !
<http://why3.lri.fr/stdlib/ref.html#prefix.20.21_22>i +
<http://why3.lri.fr/stdlib/int.html#infix.20.2B_86> 1
| Red <http://toccata.lri.fr/gallery/flag2.en.html#Red_13> -> r :=
<http://why3.lri.fr/stdlib/ref.html#infix.20:.3D_24> !
<http://why3.lri.fr/stdlib/ref.html#prefix.20.21_22>r -
<http://why3.lri.fr/stdlib/int.html#infix.20-_100> 1; swap
<http://toccata.lri.fr/gallery/flag2.en.html#swap_71> a !
<http://why3.lri.fr/stdlib/ref.html#prefix.20.21_22>r !
<http://why3.lri.fr/stdlib/ref.html#prefix.20.21_22>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.
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
> <+33%201%2069%2015%2066%2008>
> > 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
