Assertions are used to state properties which are believed to hold of
the other definitions in a script.
(FDR1 scripts adopted a convention of defining two processes
SPEC and SYSTEM, with the understanding that the check
SPEC[=SYSTEM should be performed.
This has weaknesses: the correct model for the check is not always
apparent, and some scripts require multiple checks.)
The most basic form of the definition is
assert b
where b is a boolean expression.
For example,
primes = ... take(0,_) = <> take(n,<x>^s) = <x> ^ take(n-1,s) assert <2,3,5,7,11> == take(5, primes)
It is also possible to express refinement checks (typically for use by FDR)
assert p [m= q
where p and q are processes and m denotes the model
(T, F or FD for trace, failures and failures-divergences respectively).
Similarly, we have
assert p :[ deterministic [FD] ] assert p :[ deadlock free [F] ] assert p :[ divergence free ]
for the other supported checks within FDR. Only the models F and FD may be used with the first two, with FD assumed if the model is omitted.
All assertions can be negated by prefixing them with not. This
allows scripts to be constructed where all checks are expected to
succeed (useful when a large number of checks are to be performed.)
Note that process tests cannot be used in any other context. The process assertions in a script are used to initialise the list of checks in FDR2.
Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.