Hello,
As far as I understand, the problem is more about putting data with
invariant inside a compound type like a list.
I suggest you proceed without using the invariant feature but do it "by
hand" such as
type lit = { var : int ; sign : bool }
predicate wf_lit (l:lit) = l.var >= 0
let f (ls : list lit) =
requires { forall l:lit. mem l ls -> wf_lit l } ()
- Claude
Le 06/08/2017 à 00:41, Jonathan Laurent a écrit :
> Hi,
> It seems to me that Why3 considers any record type with an invariant as
> immutable. Indeed,
> the following code gets me an error:
>
> ```
> type lit = { var : int ; sign : bool } invariant { self.var >= 0 }
>
> let f (ls : list lit) =
> requires { forall l:lit. mem l ls } ()
>
> ```
>
> Error: Cannot update values of type (list21 (lit19 <>)).
>
>
> The problem disappears if I remove the invariant of `lit`. Is this a bug
> or a feature ? Is there a way I can specify type invariants for
> immutable records.
>
> Best,
> Jonathan Laurent
>
>
> _______________________________________________
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
--
Claude Marché | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France |
Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex |
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
