Tuesday, September 14, 2010

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.

2 comments:

  1. The syntax of open intervals is quite unintuitive.

    Why not authorize instead chaining of comparisons, like done in the ACSL annotation language?
    (Consecutive comparison operators on p 16 of http://frama-c.com/download/acsl-implementation-Boron-20100401.pdf)

    So that you would write in your example:

    { A < X <= B }

    ReplyDelete
  2. Part of the desire was to provide one or more operators that produced an interval as their result, as opposed to a notation for doing a more complex comparison. When defining the range of a type, you want to "pass in" an interval over which the type will be defined. E.g:

    type Full_Circle is
       Fixed_Point< -180.0 <.. 180.0 >;

    So the challenge is to come up with a notation that indicates an open- or half-open interval. I could envision another notation such as ~.., ..~, ~..~ as a way to avoid use of the potentially confusing "<" and ">" symbols. Might the following be more intuitive/readable:

    type Full_Circle is
       Fixed_Point< -180.0 ~.. 180.0 >;

    ReplyDelete