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 τ x₁,…,τ x_n; e and existential quantification by \exists τ x₁,…,τ x_n; e.

Terms are built on

• integer and real arithmetic
• Java array access and field access
• Java cast
• user-defined logic types, and user-defined predicate and logic functions, described in Section 3.6

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:

Conditional

c ? e₁ : e₂. 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 ? e₁ : e₂ is equivalent to (c ==> e₁) && (! c ==> e₂)

Consecutive comparison operators

the construct t₁ relop₁ t₂ relop₂ t₃ ⋯ t_k with several consecutive comparison operators is a shortcut for t₁ relop₁ t₂  &&  t₂ relop₂ t₃  &&  ⋯ . 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.

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	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

Figure 3.2: Operator precedence

---

3.1.2  Semantics

The semantics of logic expressions is based on mathematical first-order logic (http://en.wikipedia.org/wiki/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:

• “Mathematical” types: integer for unbounded, mathematical integers; real for real numbers.
• Logic types introduced by specification writer (see Section 3.6).

There are implicit coercions for numeric types:

• integer types char, byte, short, int and long are all subtypes of type integer,
• integer is itself a subtype of type real,
• types float and double are subtypes of type real.

Notes:

• There is a distinction between booleans and propositions. An expression like x<y, in a term position returns a boolean, and is also allowed in a proposition position.
• Quantification can be made over any type: logic types and any Java types. Quantification over objects must be carefully designed, regarding the memory state where field accesses are done: see Section 3.1.4 and Section 3.6.2.

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:

• |d.q| ≤ |n|, and |q| is maximal for this property ;
• q is zero if |n|<|d| ;
• q is positive if |n|≥|d| and n and d have the same sign ;
• q is negative if |n|≥|d| and n and d have the opposite signs ;
• q.d+r = n ;
• |r|<|d| ;
• r is zero or has the same sign as d.

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.

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

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.

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.

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.

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:

• Precondition:
  • The caller is responsible for ensuring it before call
  • The callee assumes it at entrance of its body
• Postcondition:
  • The callee must guarantee it at normal exit
  • The caller can then assume it after the call

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:

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

• The caller must guarantee that the callee is called in a state (called prestate) where the property P₁ && P₂ holds.
• When the callee returns normally, the property E₁ && E₂ must hold in the corresponding poststate.
• All memory locations of the prestate that do not belong to the set L₁ ∪ L₂ remain allocated and are left unchanged in the poststate.

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

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

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

• \old(A) ⇒ E holds
• If \old(A) holds, each location of the pre-state not in L remains allocated and unchanged in the post-state

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 post-state:

• \old(A) ⇒ E holds
• If \old(A) holds, each location of the pre-state not in L remains allocated and unchanged in the post-state

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

3.4  Code annotations

3.4.1  Assertions

• Additional clause:
  //@ assert prop
  specify that the given property is true at the corresponding program point

3.4.2  Loop annotations

• Additional clause for loops:
  /*@ loop_invariant prop
    @ loop_assigns tset
    @*/
  specify that
  • the given property is an inductive loop invariant for the loop:
    • true at loop entrance
    • preserved by loop body
  • side-effect of the loop are included in the given tset

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

• New logic functions and predicates can be defined

3.6.2  Hybrid predicates

• Logic functions and predicates may depend on memory heap
• In such a case, logic labels are required:
• Indeed, with only one label, the following is allowed too:

3.6.3  Abstract data types

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

• a type name
• the profile of logic functions and predicates operating on it
• a set of axioms

3.7  Termination

3.7.1  Loop variants

• A loop can be annotated with a variant: an integer expression that decreases at each iteration, using the clause loop_variant.

3.8  Ghost variables