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. Best, Sandrine
signature.asc
Description: Message signed with OpenPGP
_______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club