How to define an invariant that describes a sorted sequence

[Pramod Biligiri <pramodb...@xxxxxxxxx>]

Hi,

I'm trying to define an invariant that specfies a sequence should be (strictly) ordered, and am not getting the correct syntax. My sequence is called myList and the invariant is called Ordered

define
     Ordered == \A i \in 1..Len(myList), j \in 1..Len(myList), i < j: myList[i] < myList[j]
end define;       

Thanks,

Pramod