Download Assertion Language manual - Bound

Bounds as used in several places
Another element that will occur in several syntactic forms is the definition of bounds on a
number:
Bound
®
|
|
|
|
|
|
|
|
|
integer
= integer
integer .. integer
..
integer ..
.. integer
> integer
>= integer
< integer
<= integer
A Bound defines an interval subset of the integers as follows. If a single integer is given,
possibly preceded by an equals symbol (=), the subset consists of this value only. If two
integers are given separated by two periods (..) the subset consists of the interval from the first
integer to the second integer, inclusive.
If only the two periods are given, with no integer before or after, the subset contains all values.
The rest of the forms define subsets that are bounded at only one end: If an integer is followed
by two periods (without a following second integer) the subset consists of all values greater or
equal to the given integer. Conversely, when the two periods precede the single integer the
subset consists of all values less or equal to the given integer. If a relational symbol followed by
an integer is given, the subset consists of those values that stand in the given relation to the
given integer. Thus, the Bound form “>= 4” has the same meaning as “4 ..”, and “<= 4” has the
same meaning as “.. 4”.
In some contexts, the subset can contain only non-negative values. For example, a bound on
the number of executions of a call or the number of repetitions of a loop contains an implicit
lower bound of zero even if the Bound explicitly states only an upper bound or no bound at all.
Singular and plural keywords and other alternatives
Some keywords can be written in singular or plural form, interchangeably, to make the
assertion syntax closer to normal grammar. To avoid clutter in the grammar, the grammar
rules use only one form, but the assertion text can use either form (with a few exceptions
explained later). Some verb-like keywords such as contain have a third equivalent -ing form:
containing. Moreover, a few keyword pairs have obsolete single-word equivalents with
embedded underscores. Here are the equivalent keywords:
78
First form
Equivalent second and third forms
call
contain
cycle
define
do
execute
is
loop
repeat
return
span
start
time
use
calls
contains
cycles
defines
does
executes
are
loops
repeats
returns
spans
starts
times
uses
Keyword pair
Obsolete but equivalent keyword
Syntax basics
calling
containing
defining
executing
spanning
using
Bound-T Assertion Language