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