Sorry for the noise.
Here is the example that is not accepted by why3 anymore.
I don’t understand why a[i] is expected to have type int.
Best,
Sandrine
-------------
module Mt
use int.Int
use bool.Bool
use array.Array
type cell = A | B | C
predicate p (a: array cell) (i:int) = (a[i] = A)
let f (a: array cell) (i: int) : bool
requires { 0 <= i < length a }
ensures { result <-> p a i }
=
a [i] = A
(* This expression has type Mt.cell, but is expected to have type int *)
end
> Le 10 nov. 2018 à 12:00, why3-club-requ...@lists.gforge.inria.fr a écrit :
>
> 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
