Notation for "intervals" in ParaSail

It is quite common in a precondition or postcondition to want to indicate that the value of a variable must be within some interval of values (aka "range" of values), such as 1..10, or 0..+inf.  When dealing with real values (e.g. floating point values) as opposed to integer values, it is often desirable to represent an open or half-open interval, where the boundary value is not included in the specified interval.  For example, to specify that X must be in the interval 0.0 .. 10.0, but not including zero itself, the notation "(0.0 .. 10.0]" is sometimes used, where where "(" and ")" represent an open (exclusive) boundary, while "[" and "]" represent a closed (inclusive) boundary.

For ParaSail, because "()" and "[]" are already used in the syntax, we have adopted a different notation for open and half-open intervals:

  0.0 .. 10.0       closed interval  
  0.0 <.. 10.0     half-open on left
  0.0 ..< 10.0     half-open on right
  0.0 <..< 10.0   open on both sides

Hence, one can write in an annotation:

  { X in A <.. B }

as a short-hand for

  { A < X and then X <= B }

with the additional difference that X is only evaluated once (though that will rarely matter in an annotation). 

Like the other relational operators, these interval operators are defined automatically once the "=?" operator has been appropriately defined.