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.
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 >;
I think the syntax 1..10 is too terse: the lower bound is almost certainly inclusive, but it is unclear if the upper bound is inclusive or exclusive. (Note that this is important for ints as well as floats, particularly ints used as indices.) I think the list-comprehension syntax is fine, even if only special cases like {x | a < x < b}, {x | a <= x < b}, are allowed. Sometimes orthogonality is too much.
ReplyDeleteCertainly any notation needs to be learned. In our experience, by providing four syntaxes: A .. B, A <.. B, A ..< B, and A <..< B, there becomes no doubt that A .. B is a closed interval, while the others are half-open or open intervals. These work for integers, floats, strings, or any type for which the comparison operator is defined.
Delete