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 constant empty_state = { contents = Nil }
This works in master (and a proper VC is produced), but probably not in the
released versions: verification of top-level computations is currently work
in progress in Why3. Thus passing by f_init is probably your best bet at
the moment.
Best,
Andrei
On 12 November 2018 at 16:52, Julia Lawall <julia.law...@lip6.fr> wrote:
> 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_init needed? Without it, ie with the code in
> comments in place of the call to f_init, I get a syntax error about
> contents not being a record field. Should contents be referred to in
> another way?
>
> thanks,
> julia
> _______________________________________________
> 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
