This chapter is the reference for the specification language. It is unfortunately largely incomplete, but for missing parts and explanations we refer to the ACSL Reference Manual [2], which is very close.
We present the language of expressions one can use in annotations. These are called logic expressions.
This language is essentially the standard multisorted firstorder logic. It is a twovalued logic language, made of propositions with standard firstorder connectives, built upon a language of atoms called terms.
As far as possible, the syntax of Java expressions is reused:
conjunction is denoted as &&
, disjunction as 
and
negation as !
. Additional connectives are ==>
for
implication, <==>
for equivalence. Universal quantification is
denoted by \forall τ x_{1},…,τ x_{n}; e and existential
quantification by \exists τ x_{1},…,τ x_{n}; e.
Terms are built on
In essence, terms correspond to pure Java expressions, with additional constructs that we will introduce progressively, except that method and constructor calls are not allowed.
Figure 3.1 presents the grammar for the basic construction of logic expressions.
Basic additional constructs are as follows:
==>
e_{1}) &&
(!
c ==>
e_{2})&&
t_{2} relop_{2} t_{3} &&
⋯ .
Nevertheless, it is required that the relop_{i} operators must be in
the same “direction”, i.e. they must all belong either to
{<
, <=
, ==
} or to
{>
,>=
,==
}. For example, expressions
x < y > z
and x != y != z
are forbidden.The precedence of Java operators is conservatively extended with additional operators, as shown Figure 3.2. In this table, operators are sorted from highest to lowest priority. Operators of same priority are presented on the same line.
class associativity operators selection left [
⋯]
.
unary right !
~
+

(cast)multiplicative left *
/
%
additive left +

shift left <<
>>
>>>
comparison left <
<=
>
>=
comparison left ==
!=
bitwise and left &
bitwise xor left ^
bitwise or left 
connective and left &&
connective xor left ^^
connective or left 
connective implies right ==>
connective equiv left <==>
ternary connective right ⋯ ?
⋯:
⋯binding left \forall \exists
The semantics of logic expressions is based on mathematical firstorder logic (http://en.wikipedia.org/wiki/First_order_logic), thus it is a 2valued logic with only total functions. Consequently, expressions are never “undefined”.
This design choice has to be emphasized because it is not straightforward, and specification writer should be aware of that. The issues are shared with JML. A comprehensive list of issues has been compiled by Patrice Chalin [3, 4].
The choice of having only total functions allows to write for example
the term 1/0
, or p.f
when p is null, or t[n]
where n is outside the array bounds. In
particular, the predicates

are true, since they are instances of the general axiom ∀ x,
x==
x of firstorder logic.
So, it is up to the writer of specification to take care of writing consistent assertions.
The language of logic expressions is typed (as for multisorted firstorder logic). Types are either Java types or logic types defined as follows:
integer
for unbounded,
mathematical integers; real
for real numbers.
There are implicit coercions for numeric types:
char
, byte
, short
, int
and
long
are all subtypes of type integer
,
integer
is itself a subtype of type real
,
float
and double
are subtypes of type real
.
Notes:
The following integer arithmetic operations apply to mathematical integers: addition, subtraction, multiplication, unary minus, division and modulo. The value of a Java variable of an integer type is promoted to a mathematical integer. As a consequence, there is no such thing as “overflow” in logic expressions.
For division and modulo, the results are not specified if divisor is zero, otherwise if q and r are the quotient and the remainder of n divided by d then:
5/3
is 1 and 5%3
is 2
(5)/3
is 1 and (5)%3
is 2
5/(3)
is 1 and 5%(3)
is 2
(5)/(3)
is 1 and (5)%(3)
is 2
Hexadecimal and octal constants always denote nonnegative integers.
In logic expressions, casting operations from mathematical integers towards a Java integer type t (among char, byte, short, int and long) is allowed, and is interpreted as follows: the result is the unique value of the corresponding type that is congruent to the mathematical result modulo the cardinal of this type.
If one wants to express, in the logic, the result of the Java computations of an expression, one should add all necessary casts. For example, the logic expression which denotes the result of Java computation of x*y+z is (int)((int)(x*y)+z).
Remark: implicit casts from integers to Java integer type are forbidden.
Quantification can be either on mathematical integer
or bounded
types short
, char
, etc. In the latter case,
quantification corresponds to integer quantification over the
corresponding interval.
\forall byte b; b <= 1000
\forall integer b; 128 <= b <= 127 ==> b <= 1000
Like arithmetic operations, bitwise operations apply to any mathematical integers: any mathematical integer as a unique infinite 2complement binary representation with infinitely many 0 (for nonnegative numbers) or 1 (for negative numbers) on the left. Then bitwise operations apply to these representation.
7 & 12
= ⋯ 00111 &
⋯ 001100 =
⋯ 00100 = 4
8  5
= ⋯ 11000 
⋯ 00101 = ⋯
11101 = 3
~5
= ~
⋯ 00101 = ⋯ 111010 = 6
5 << 2
= ⋯ 11011 <<
2 = ⋯
11101100 = 20
5 >> 2
= ⋯ 00101 >>
2 = ⋯ 0001 = 1
5 >> 2
= ⋯ 11011 >>
2 = ⋯ 1110 =
2
Floatingpoint constants and operations are interpreted as mathematical real numbers. A Java variable of type float or double is implicitly promoted to a real. Integers are promoted to reals if necessary.
Comparisons operators are interpreted as real operators too.
A simple contract is an annotation that can be given to constructors and methods (not depending on whether they are given a body or are abstract). It is a contract between the caller and the callee, made of a precondition and a postcondition:
Additionally, a contract can be completed with a frame clause which describes sideeffects, and acts as a postcondition.
Note that postconditions of simple contracts only concern normal exit: exiting with exceptions can be specified using additional behavior clauses described in Section 3.3
contract ::= (requiresclause ∣ assignsclause ∣ ensuresclause ) ^{*} requiresclause ::= requires proposition ; assignsclause ::= assigns locations ; locations ::= location (, location) ^{*} ∣ \nothing ensuresclause ::= ensures proposition ;
The syntax of simple contracts syntax is given Figure 3.3. Let’s consider a simple contract of the following generic form:
the semantics of such a contract can be rephrased as follows:
&&
P_{2} holds.
&&
E_{2} must hold in the corresponding poststate.
Thus, the contract above is equivalent to the following simplified one:
&&
P_{2}; &&
E_{2}; The multiplicity of clauses are proposed mainly to improve readibility. Also, if no clause requires is given, it defaults to requiring ‘true’, and similarly for ensures clause. Giving no assigns clause means that sideeffects are not specified: it potentially modifies everything.
A simple contract can be augmented with behaviors.
A normal behavior clause as the form
The semantics of such a behavior is as follows. The callee guarantees that if it returns normally, then in the poststate:
An exceptional behavior clause as the form
The semantics of such a behavior is as follows. The callee guarantees that if it exits with exception Exc, then in the poststate:
Notice that in E, \result is bound to the exception object thrown.
A class invariant is a property attached to a class. This property is supposed to hold on any object of that class. More precisely, it holds at method entrance and exit, and at the exit of constructor.
New logic data types (i.e. immutable) can be introduced abstractly by giving
loop_variant
.