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.
thanks, julia _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
