On 2018-11-12 22:05, Guillaume Melquiond
writes:
This is interesting. What was the motivation to remove
polymorphic
equality?
There are several reasons. One of them is that logical equality
(the
polymorphic one) does not coincide with program equality (a la
OCaml) in
presence of ghost
Le 12/11/2018 à 13:10, Alan Schmitt a écrit :
Hello,
On 2018-11-12 09:05, Claude Marché writes:
Since Why3 1.0, there is no polymorphic equality in programs. Hence
there is no symbol (=) for type cell in your code, but only the equality
for type int.
This is interesting. What was the
Hello,
On 2018-11-12 09:05, Claude Marché
writes:
Since Why3 1.0, there is no polymorphic equality in programs.
Hence
there is no symbol (=) for type cell in your code, but only the
equality
for type int.
This is interesting. What was the motivation to remove polymorphic
equality?
Best
Since Why3 1.0, there is no polymorphic equality in programs. Hence
there is no symbol (=) for type cell in your code, but only the equality
for type int.
The standard workaround is to declare such an equality function as
val (=) (x y:cell) : bool
ensures { result <-> x=y }
of course one
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] =
