Hi Sandrine,
It looks like you forgot the first parameter "a" of "p" in "result <-> p
i". When I add it, this is accepted (and proved) with the most recent
version of Why3.
--
Jean-Christophe
On 11/9/18 6:20 PM, Sandrine Blazy wrote:
> Hi,
>
> the following example worked fine using why3 version 0.87.3.
> How should I write it so that it becomes accepted by why3 version 1.1.0 ?
>
> module M
> use int.Int
> use bool.Bool
> use array.Array
>
> predicate p (a: array int) (i:int) = (a[i]=0)
>
> let f (a: array int) (i: int) : bool
> requires { 0 <= i < length a }
> ensures { result <-> p i}
> =
> a[i] = 0
>
> end
> _______________________________________________
> 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
