Hi Sandrine,

On 11 March 2018 at 17:46, Sandrine Blazy <sandrine.bl...@irisa.fr> wrote:

> Hi,
>
> I would like to define a type invariant related to an array type.
> If I write for example :
>     type myarray = array int
>     invariant { forall i:int. 0 <=i< length self -> my_predicate self[i] }
>
> then I get the following error message:
>     type aliases cannot have invariants.
>
> So, I changed my definition to the following one :
>     type tmyarray = { myarray : array int }
>     invariant { forall i:int. 0 <= i < length self.myarray ->
>                   my_predicate (self.myarray[i]) }
>
> This definition is ok, but the use of a record requires to construct and
> destruct many of such records in my spec and my code. So, I am wondering
> if there is a better way to define my type invariant.
>

unfortunately, not. The simplification routines will probably eliminate
most of these constructors/destructors, but you would still need to write
them. Otherwise, you should state the invariant manually in the
pre-/post-conditions.

Best,
Andrei
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Reply via email to