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.



Attachment: signature.asc
Description: Message signed with OpenPGP

Why3-club mailing list

Reply via email to