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 fie
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 motiva
On Mon, 12 Nov 2018, Andrei Paskevich wrote:
> Types with invariants cannot be constructed in logic, because Why3 does not
> generate verification conditions for logic declarations. When you write a
> record constructor in program code, as in f_init, the invariant becomes part
> of the VC.
>
> N
Types with invariants cannot be constructed in logic, because Why3 does not
generate verification conditions for logic declarations. When you write a
record constructor in program code, as in f_init, the invariant becomes
part of the VC.
Normally, you should be able to write simply:
let constan
I have the following code:
type state = { contents : list thread }
invariant { Distinct.distinct contents /\ valid_state contents }
by { contents = Nil }
let function f_init () = { contents = Nil }
constant empty_state : state = f_init () (* { contents = Nil } *)
Why is the function f_in
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
