Previous Up Next

Chapter 3  Specification Language: Reference

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.

3.1  Logic expressions

We present the language of expressions one can use in annotations. These are called logic expressions.

This language is essentially the standard multi-sorted first-order logic. It is a two-valued logic language, made of propositions with standard first-order 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 τ x1,…,τ xn; e and existential quantification by \exists τ x1,…,τ xn; 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.

rel-op ::= ==    ∣   !=    ∣   <=    ∣   >=    ∣   >    ∣   <   
bin-op ::= +    ∣   -    ∣   *    ∣   /    ∣   %   
  &&    ∣   ||    ∣ boolean operations  
  &    ∣   |  bitwise operations  
  ==>  boolean implication  
  <==>  boolean equivalence  
unary-op ::= +    ∣   -  unary plus and minus  
  !  boolean negation  
  ~  bitwise complementation  
lexpr ::= true    ∣   false   
  integer integer constants  
  real real constants  
  id variables  
  unary-op   lexpr  
  lexpr   bin-op   lexpr  
  lexpr   (rel-op   lexpr)+ comparisons, see remark below  
  lexpr   [    lexpr   ]  array access  
  lexpr   .    id object field access  
  (    type-expr   )    lexpr cast  
  id   (    lexpr   (,    lexpr)*   )  function application  
  (    lexpr   )  parentheses  
  lexpr   ?    lexpr   :    lexpr  
  \forall    binders   ;    lexpr universal quantification  
  \exists    binders   ;    lexpr existential quantification  
binders ::= type-expr   variable-ident+  
    (,    variable-ident+)*  
type-expr ::= logic-type-expr   ∣   Java-type-expr  
logic-type-expr ::= built-in-logic-type  
  id logic type identifier  
built-in-logic-type ::= integer    ∣   real    
variable-ident ::= id    ∣   variable-ident   [] 
Figure 3.1: Grammar of logic expressions

Basic additional constructs are as follows:

c ? e1 : e2. There is a subtlety here: the condition may be either a boolean term or a proposition. In case of a proposition, the two branches must be also proposition, so that this construct acts as a connective with the following semantics: c ? e1 : e2 is equivalent to (c ==> e1) && (! c ==> e2)
Consecutive comparison operators
the construct t1 relop1 t2 relop2 t3tk with several consecutive comparison operators is a shortcut for t1 relop1 t2  &&  t2 relop2 t3  &&  ⋯ . Nevertheless, it is required that the relopi 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.

3.1.1  Operator precedence

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 associativityoperators
selectionleft[] .
unary right! ~ + - (cast)
multiplicativeleft* / %
additiveleft+ -
shift left<< >> >>>
comparisonleft< <= > >=
comparisonleft== !=
bitwise andleft&
bitwise xorleft^
bitwise orleft|
connective andleft&&
connective xorleft^^
connective orleft||
connective impliesright==>
connective equivleft<==>
ternary connectiveright?:
bindingleft\forall \exists
Figure 3.2: Operator precedence

3.1.2  Semantics

The semantics of logic expressions is based on mathematical first-order logic (, thus it is a 2-valued 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 first-order logic.

So, it is up to the writer of specification to take care of writing consistent assertions.

3.1.3  Typing

The language of logic expressions is typed (as for multi-sorted first-order logic). Types are either Java types or logic types defined as follows:

There are implicit coercions for numeric types:


3.1.4  Integer arithmetic and machine integers

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:

Example 1   The following examples illustrates the results of division and modulo depending on signs of arguments:

Hexadecimal and octal constants

Hexadecimal and octal constants always denote non-negative integers.

Casts and overflow

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.

Example 2   (byte)1000 is 1000 mod256 i.e. −24.

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.

Example 3   The formula
\forall byte b; b <= 1000
is valid since it is equivalent to
\forall integer b; -128 <= b <= 127 ==> b <= 1000

Bitwise operations

Like arithmetic operations, bitwise operations apply to any mathematical integers: any mathematical integer as a unique infinite 2-complement binary representation with infinitely many 0 (for non-negative numbers) or 1 (for negative numbers) on the left. Then bitwise operations apply to these representation.

Example 4  

3.1.5  Real numbers and floating point numbers

Floating-point 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.

Example 5   2 * 3.5 denotes the real number 7

Comparisons operators are interpreted as real operators too.

3.2  Simple contracts

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 side-effects, and acts as a postcondition.

Note that post-conditions of simple contracts only concern normal exit: exiting with exceptions can be specified using additional behavior clauses described in Section 3.3

contract ::= (requires-clause   ∣   assigns-clause   ∣   ensures-clause ) *  
requires-clause ::= requires    proposition   ;   
assigns-clause ::= assigns    locations   ;   
locations ::= location   (,    location*   ∣   \nothing   
ensures-clause ::= ensures    proposition   ; 
Figure 3.3: Grammar of simple contracts

The syntax of simple contracts syntax is given Figure 3.3. Let’s consider a simple contract of the following generic form:

/*@ requires P1;
  @ requires
  @ assigns
  @ assigns
  @ ensures
  @ ensures

the semantics of such a contract can be rephrased as follows:

Thus, the contract above is equivalent to the following simplified one:

/*@ requires P1 && P2;
  @ assigns
  @ ensures
E1 && E2;

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 side-effects are not specified: it potentially modifies everything.

3.3  Behavior clauses

A simple contract can be augmented with behaviors.

A normal behavior clause as the form

0pt behavior id : 
assumes A ; 
assigns L ; 
ensures E ; 

The semantics of such a behavior is as follows. The callee guarantees that if it returns normally, then in the post-state:

An exceptional behavior clause as the form

0pt behavior id : 
assumes A ; 
assigns L ; 
signals (ExcE ; 

The semantics of such a behavior is as follows. The callee guarantees that if it exits with exception Exc, then in the post-state:

Notice that in E, \result is bound to the exception object thrown.

3.4  Code annotations

3.4.1  Assertions

3.4.2  Loop annotations

3.5  Data invariants

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.

3.6  Advanced modeling language

3.6.1  Logic definitions

3.6.2  Hybrid predicates

3.6.3  Abstract data types

New logic data types (i.e. immutable) can be introduced abstractly by giving

3.7  Termination

3.7.1  Loop variants

3.8  Ghost variables

Previous Up Next