Information Technology Reference
In-Depth Information
a)
b)
1
#include
<limits.h>
2
/
*
@
requires
x > INT_MIN;
3
1
#include
<limits.h>
2
/
*
@
requires
x > INT_MIN;
3
assigns \nothing
;
behavior
pos:
4
ensures
(x >= 0 ==>
\result
== x) &&
assumes
x>=0;
5
(x < 0 ==>
\result
== -x);
ensures \result
== x;
4
6
assigns \nothing
;
behavior
neg:
5
7
6
*
/
7
int
absval(
int
x){
8
assumes
x<0;
8
ensures \result
== -x;
9
return
(x>=0)?x:(-x);
10
*
/
11
int
absval(
int
x){
12
9
}
return
(x>=0)?x:(-x);
13
}
Fig. 2.
Two ways to specify function
absval
with an e-acsl contract
Specifying assertions in a programming language like C has several drawbacks.
First, complex properties (e.g. with quantifications and different behaviors) can
be dicult to specify and to check, may require significant additional program-
ming effort and appear to be error-prone themselves. Comparing computed val-
ues with initial or intermediate ones may need storing some values in additional
auxiliary variables. Some arithmetic properties (e.g. absence of overflows after
an arithmetic operation) are simpler to express in a specification language with
mathematical integers than using bounded machine integers in C. Second, clear
separation of the code required only for assertion checking and the functional
code may be desirable to optimize performances of the final release, but it often
remains manual, even if preprocessor or configuration options may help to ex-
clude assertion related statements in a particular build. Mixing both can make
source code more heavy and less readable. Third, absence of unintended side-
effects cannot be automatically ensured for assertion checking code written in
C. Finally, the usage of resulting C assertions is limited to runtime verification
and cannot be extended to verification techniques requiring formal specifications
(such as proof of programs).
Other specification formalisms offer more expressive notations compatible
with formal verification, for example, Eiffel [8], JML [9], Spec# [10], SPARK
2014 [11] (see [1] for other references). One of them is the e-acsl specification
language [5,6].
e-acsl can express the C assertions of Fig. 1a using the
assert
clause as shown
in Fig. 1b. However, e-acsl language is much more expressive than C assertions.
Indeed, in addition to C expressions and occasional assertions (like in Fig. 1b),
an e-acsl specification can include function contracts with preconditions and
postconditions, behaviors, first-order logic predicates (with quantifications over
finite intervals of integer values), mathematical integers (translated into C us-
ing GMP library
1
when required), references to the value of a variable or an
expression at a particular program point (e.g. a label), memory-related clauses
(specifying pointer validity, offset, memory block properties), etc. An e-acsl
clause cannot contain side-effects, so there is no risk to introduce an unintended
