Information Technology Reference
In-Depth Information
Locomotive
Vigilance_device
unsigned int actual_time
unsigned int speed
int standstill
int train_brake
int forced_brake
unsigned int button_start_time
unsigned int button_end_time
int button_status
Fig. 3. Data Structures.
forced_brake
are represented by an integer, but contain the Boolean values
true or false, where
1
denotes
TRUE
and
0
denotes
FALSE
.
The structure
Vigilance_device
contains the variables
button_start_time
and
button_end_time
describing the moments a vigilance device pedal or
button was invoked and released the last time. The variable
button_status
represents a Boolean variable, which is true if any vigilance device pedal or
button is currently invoked.
3.1
An Introduction to ACSL
ACSL annotations are expressed in special C-comments
/
*
@...
*
/
as a
multi-line comment or
//@...
as a single-line comment. A function con-
tract declares a set of
requires
clauses, stating the properties the function
may expect on entry, and a set of
ensures
clauses, stating the properties the
function must satisfy upon exit.
Properties are formulas denoted in a language close to
C
itself. For ex-
ample, equality, negation, and conjunction are denoted by
==
,
!
,and
&&
,
respectively; binding-priorities are as in
C
. In addition, the weaker-binding
junctors
==>
and
<==>
denote implication and equivalence. Moreover, rela-
tion chains familiar from mathematical notation, such as,
0<=i<n
,may
be used.
Function parameters and visible variables may appear in formulas, they
refer, by default, to their values on entry and exit in a
requires
and
ensures
clause, respectively. The notation
\at(v,L)
refers to the value of
v
at the
program point corresponding to the
C
-label
L:
. A predefined label
Old
allows
one to refer to on-entry values in
ensures
clauses too,
\old(EXPR)
being an
abbreviation for
\at(EXPR,Old)
. The label
Here
refers to the on-exit value
in an
ensures
clause.
A macro-like mechanism, the
predicate
definition allows users to abbre-
viate arbitrary formulas by a parametrized name. Parameters may be of
C
types or logical types enclosed in parentheses). They may also denote memory
states at certain labels enclosed in curly braces.
3.2
Using ACSL
Due to some informal requirements some variables may only take on Boolean
values, i.e.,
1
represented as
TRUE
and
0
represented as
FALSE
.However,
