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.
>
> 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.
OK, thanks!
julia
>
> 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
