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
