*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.

The syntax of open intervals is quite unintuitive.

ReplyDeleteWhy 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 }

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:

ReplyDeletetype 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 >;