13. Statements and Annotation Statements

JML also defines a number of annotation statements that may be interspersed with Java statements in the body of a method, constructor, or initialization block.

The following gives the syntax of statements. These are the standard Java statements, with the addition of annotations, the hence-by-statement, assert-redundantly-statement, assume-statement, set-statement, unreachable-statement, debug-statement, and the various forms of model-prog-statement. See section 15. Model Programs, for the syntax of model-prog-statement, which is only allowed in model programs. [[[ Does this include local class declarations?]]]

compound-statement ::= { statement [ statement ] ... } statement ::= compound-statement | local-declaration ; | ident : statement | expression ; | if ( expression ) statement [ else statement ] | possibly-annotated-loop | break [ ident ] ; | continue [ ident ] ; | return [ expression ] ; | switch-statement | try-block | throw expression ; | synchronized ( expression ) statement | ; | jml-annotation-statement | assert-statement | jml-annotation-statement | model-prog-statement // only allowed in model programs switch-statement ::= switch ( expression ) { [ switch-body ] ... } switch-body ::= switch-label-seq [ statement ] ... switch-label-seq ::= switch-label [ switch-label ] ... switch-label ::= case expression : | default : try-block ::= try compound-statement [ handler ] ... [ finally compound-statement ] handler ::= catch ( param-declaration ) compound-statement

The semantics of the Java statements are as in Java [Arnold-Gosling-Holmes00] [Gosling-etal00]. More details on the JML-specific features related to statements are described below.

13.1 Local Declaration Statements
13.2 Loop Statements
13.3 Assert Statements
13.4 JML Annotation Statements

13.1 Local Declaration Statements

The following is the syntax of local declaration statements. See section 7.1.2 Field and Variable Declarations, for the syntax of variable-decls.

local-declaration ::= local-modifiers variable-decls

13.1.1 Modifiers for Local Declarations

13.1.1 Modifiers for Local Declarations

JML allows the modifiers ghost, uninitialized, non_null and nullable in addition to Java's final modifier on local variable declarations. See section 18. Universe Type System, for the grammar of ownership-modifier.

local-modifiers ::= [ local-modifier ] ... local-modifier ::= ghost | final uninitialized | non_null | nullable | ownership-modifier // when the Universe type system is on

The JML modifiers are discussed to some extent below. See section 7.1.2.1 JML Modifiers for Fields, for more about these modifiers.

When used as a local variable modifier, uninitialized means that the variable should be considered by the tools to be uninitialized, even if it has an initialization. This allows the tools to check for uses before a "real" initialization.

A local ghost declaration is a variable declaration with a ghost modifier, entirely contained in an annotation. It introduces a new variable that may be used in subsequent annotations within the remainder of the block in which the declaration appears. A ghost variable is not used in program execution as Java variables are, but is used by runtime assertion checkers or a static checker to reason about the execution of the routine body in which the ghost variable is used.

• The variable name may not be already declared as a local variable or local ghost variable or as a formal parameter of the routine in which the declaration appears.
• Each variable declared may have an initializer; the initializer is in the scope of the newly declared variable. Furthermore, since the initializer is in an annotation (and thus not executed when runtime assertion checks are turned off), the initializer of a ghost variable must be a pure expression (i.e., it must be side effect free).
• The modifiers final, uninitialized, non_null and nullable may be used on the ghost declaration.

In the following, the body of the method ghostLocalExample contains several examples of local ghost declarations.

package org.jmlspecs.samples.jmlrefman; public abstract class GhostLocals { void ghostLocalExample() { //@ ghost int i = 0; //@ ghost int zero = 0, j, k = i+3; //@ ghost float[] a = {1, 2, 3}; //@ ghost Object o; //@ final ghost non_null Object nno = new Object(); } }

13.2 Loop Statements

The following is the syntax of loop statements.

possibly-annotated-loop ::= [ loop-invariant ] ... [ variant-function ] ... [ ident : ] loop-stmt loop-stmt ::= while ( expression ) statement | do statement while ( expression ) ; | for ( [ for-init ] ; [ expression ] ; [ expression-list ] ) statement | for ( modifiers type-spec ident : expression ) statement for-init ::= local-declaration | expression-list

In JML a loop statement can be annotated with one or more loop invariants, and one or more variant functions. The following class contains an example in the middle of the method sumArray. This example has a while loop with two loop invariants, which follow the keyword maintaining, and a single variant function, which follows the keyword decreasing. The invariants and variant function are written above the loop itself. The first loop invariant describes the range that the variable i can take, and the second relates i and the value in sum.

package org.jmlspecs.samples.jmlrefman; /** An example of some simple loops with loop invariants * and variant functions specified. */ public abstract class SumArrayLoop { /** Return the sum of the argument array. */ /*@ old \bigint sum = @ (\sum int j; 0 <= j && j < a.length; (\bigint)a[j]); @ requires Long.MIN_VALUE <= sum && sum <= Long.MAX_VALUE; @ assignable \nothing; @ ensures \result == sum; @*/ public static long sumArray(int [] a) { long sum = 0; int i = a.length; /*@ maintaining -1 <= i && i <= a.length; @ maintaining sum @ == (\sum int j; @ i <= j && 0 <= j && j < a.length; @ (\bigint)a[j]); @ decreasing i; @*/ while (--i >= 0) { sum += a[i]; } //@ assert i < 0 && -1 <= i && i <= a.length; //@ hence_by (i < 0 && -1 <= i) ==> i == -1; //@ assert i == -1 && i <= a.length; //@ assert sum == (\sum int j; 0 <= j && j < a.length; (\bigint)a[j]); return sum; } }

At the end of the loop, the negation of the loop's test expression and the loop invariants hold. This is shown by the assertions after the loop.

Loop invariants and variant functions are discussed in more detail below. (Thanks to K. Rustan M. Leino, Claude Marche, and Steve M. Shaner for discussions on this topic, including details of the semantics.)

13.2.1 Loop Invariants
13.2.2 Loop Variant Functions

13.2.1 Loop Invariants

A loop can specify one or more loop invariants, using the following syntax.

loop-invariant ::= maintaining-keyword predicate ; maintaining-keyword ::= maintaining | maintaining_redundantly | loop_invariant | loop_invariant_redundantly

A loop-invariant is used to help prove partial correctness of a loop statement.

The meaning of a loop, which does not contain a use of break that exits the loop itself (as opposed to some inner loop), such as

//@ maintaining J; while (B) { S }

is as follows.

while (true) { //@ assert J; if (!(B)) { break; } S }

So that the loop invariant holds at the beginning of each iteration of the loop.

The rule for deducing what is true after the loop can be stated simply if the loop does not contain any break statements that exit the loop, and if the loop test, B, is both a Java expression and a JML specification-expression (see section 12.2 Specification Expressions). (This means that B is side-effect free.) For such loops, the rule is that, after a loop with condition B and invariant J the negation of the condition, (!B), conjoined with the invariant, J, holds. This is summarized in the following program schema.

//@ maintaining J; while (B) { // assuming B has no side effects S } // assert !(B) && J;

If the loop contains a break statement that exits the loop itself, then more detailed reasoning is necessary to establish what will be true after the loop. The intended condition that should be true after the loop when it is exited via a break statement can be recorded in the code using an assert statement. For example, if the loop has the form:

//@ maintaining J; while (true) { S1 if (C) { S2 //@ assert Q; break; } S3 }

then after the loop the asserted condition, Q, should hold, assuming there are no other break statements that exit the loop.

13.2.2 Loop Variant Functions

A loop can also specify one or more variant functions, using the following syntax.

variant-function ::= decreasing-keyword spec-expression ; decreasing-keyword ::= decreasing | decreasing_redundantly | decreases | decreases_redundantly

A variant-function is used to help prove termination of a loop statement. It specifies an expression of type long or int that must be no less than 0 when the loop is executing, and must decrease by at least one (1) each time around the loop.

The meaning of a loop such as

//@ decreasing E; while (B) { S }

in which S does not use continue, is as follows.

while (true) { long vf = E; // assuming vf is a fresh variable name if (!(B)) { break; } //@ assert 0 <= vf; S //@ assert E < vf; }

If the loop contains a continue statement, then the loop variant is checked just before each use of continue. For example, if the loop has the form:

//@ decreasing E; while (B) { S1 if (C) { S2 continue; } S3 }

then the meaning is as follows.

while (true) { long vf = E; // assuming vf is a fresh variable name if (!(B)) { break; } //@ assert 0 <= vf; S1 if (C) { S2 //@ assert E < vf; continue; } S3 //@ assert E < vf; }

13.3 Assert Statements

The syntax of assert and redundant assert statements is as follows.

assert-statement ::= assert expression [ : expression ] ; | assert predicate [ : expression ] ; assert-redundantly-statement ::= assert_redundantly predicate [ : expression ] ;

Note that Java (as of J2SDK 1.4) also has its own assert statement. For this reason JML distinguishes between assert statements that occur inside and outside annotations.

Outside an annotation, an assert statement is a Java assert statement, whose syntax follows the first assert-statement production above. Thus in such an assert statement, the first expression can have side effects (potentially, although it shouldn't). The second expression is supposed to have type String, and will be used in a message should the assertion fail.

Inside an annotation, an assert statement is a JML assert statement, and the second syntax is used for assert-statement. Thus instead of an expression before the optional colon, there is a JML predicate. This predicate cannot have side effects, but can use the various JML extensions to the Java expression syntax (see section 12.2 Specification Expressions, for details.) As in a Java assert statement, the optional expression that follows the colon must be a String, which is printed if the assertion fails.

An assert statements tells JML to check that the specified predicate is true at the given point in the program. The runtime assertion checker checks such assertions during execution of the program, when control reaches the assert statement. Other tools, such as verification tools, will try to prove that the assertion always holds at that program point, for every possible execution.

The assert-redundantly-statement must appear in an annotation. It has the same semantics as the JML form of an assert statement, but is marked as redundant. Thus it would be used to call attention to some property, but need not be checked.

13.4 JML Annotation Statements

The following gives the syntax of JML annotation statements. These can appear anywhere in normal Java code, but must be enclosed in annotations. See section 13.3 Assert Statements, for the syntax of the assert-redundantly-statement. See section 15. Model Programs, for the syntax of additional statements that can only be used in model programs.

jml-annotation-statement ::= assert-redundantly-statement | assume-statement | hence-by-statement | set-statement | refining-statement | unreachable-statement | debug-statement

13.4.1 Assume Statements
13.4.2 Set Statements
13.4.3 Refining Statements
13.4.4 Unreachable Statements
13.4.5 Debug Statements
13.4.6 Hence By Statements

13.4.1 Assume Statements

The syntax of an assume statement is as follows. As in a Java assert statement, the optional expression that follows the colon must be a String, which is printed if the assumption fails.

assume-statement ::= assume-keyword predicate [ : expression ] ; assume-keyword ::= assume | assume_redundantly

In runtime assertion checking, assumptions are checked in the same way that assert statements are checked (see section 13.3 Assert Statements).

However, in static analysis tools, the assume statement is used to tell the tool that the given predicate is assumed to be true, and thus need not be checked.

13.4.2 Set Statements

The syntax of a set statement is as follows. See section 12.3 Expressions, for the syntax of assignment-expr.

set-statement ::= set assignment-expr ;

A set statement is the equivalent of an assignment statement but is within an annotation. It is used to assign a value to a ghost variable or to a ghost field. A set statement serves to assist the static checker in reasoning about the execution of the routine body in which it appears. Note that:

• the target of the set statement must be a ghost variable or a ghost field, and
• the right-hand-side of the assignment-expr must be a pure expression (i.e., it must not have side effects).

        //@ set i = 0;
        //@ set collection.elementType = \type(int);

The reason that right hand side of the assignment-expr must be pure is because set-statements are not part of the normal Java code, but only occur in annotations. Hence they must not affect normal Java code execution, but only have side effects on the ghost field or ghost variable being assigned. This restriction is a conservative way to guarantee that property.

13.4.3 Refining Statements

The syntax of a refining statement is as follows. See section 15.6 Specification Statements, for the syntax of spec-statement and generic-spec-statement-case. See section 13. Statements and Annotation Statements, for the syntax of statement.

refining-statement ::= refining spec-statement statement | refining generic-spec-statement-case statement

A refining statement allows one to annotate a specification with a specification. It has two parts, a specification and a body. The specification part can be either a spec-statement (see section 15.6 Specification Statements), which includes the grammar for a heavyweight specification case, or a generic-spec-statement-case (see section 15.6 Specification Statements), which includes the grammar for a lightweight specification case. The body is simply a statement. In particular, the body can be a compound-statement or a jml-annotation-statement, including a nested refining-statement.

Annotating the body with a specification is a way of collecting all the specification information about the statement in one place. Giving such an annotation is especially useful for framing, e.g., writing assignable-clauses. For example, by using a refining statement, one can write an assignable clause for a loop statement or for the statement in the body of a loop.

Refining statements are also used in connection with model program specification cases (see section 15. Model Programs). Within the implementation of a method with such a model program specification, a refining statement indicates exactly what spec-statement is implemented by its body, since its specification part would be exactly that spec-statement. This is helpful for "matching" the implementation against the model program specification [Shaner-Leavens-Naumann07].

Note that the scope of any declarations made in the specification part of a refining statement are limited to the specification part, and do not extend into the body. Thus a refining statement is type correct if each of its subparts is type correct, using the surrounding context for separately type checking the specification and body.

The meaning of a refining statement of the form refining S B is that the body B must refine the specification given in S. This means that B has to obey all the specifications given in S. For example, B may not assume a stronger precondition than that given by S. (Standard defaults are used for omitted clauses in the specification part of a refining statement; thus, if there is no requires clause in a spec-statement, then the precondition defaults to true.) Similarly, B may not assign to locations that are not permitted to be assigned to by S, and, assuming S's precondition held, then when B terminates normally it must establish S's normal postcondition. See section 9. Method Specifications, for more about what it means to satisfy such a specification.

When \old() or \pre() are used in the specification part of a refining statement, they have the same meaning as in a specification statement (see section 15.6 Specification Statements).

In execution, a refining statement of the form refining S B just executes its body B. For this reason, typically the refining keyword and the specification S would be in JML annotations, but the body B would be normal Java code (outside of any annotation).

See section 15. Model Programs, for more examples.

13.4.4 Unreachable Statements

The syntax of the unreachable statement is as follows.

unreachable-statement ::= unreachable ;

The unreachable statement is an annotation that asserts that the control flow of a routine will never reach that point in the program. It is equivalent to the annotation assert false. If control flow does reach an unreachable statement, a tool that checks (by reasoning or at runtime) the behavior of the routine should issue an error of some kind. The following is an example:

if (true) { ... } else { //@ unreachable; }

13.4.5 Debug Statements

The syntax of the debug statement is as follows. See section 12.3 Expressions, for the syntax of expression.

debug-statement ::= debug expression ;

A debug statement is the equivalent of an expression statement but is within an annotation. Thus, features visible only in the JML scope can also appear in the debug statement. Examples of such features include ghost variables, model methods, spec_public fields, and JML-specific expression constructs, to name a few.

The main use of the debug statement is to help debugging specifications, e.g., by printing the value of a JML expression, as shown below.

//@ debug System.err.println(x);

In the above example, the variable x may be a ghost variable. Note that using System.err automatically flushes output, unlike System.out. This flushing of output is helpful for debugging.

As shown in the above example, expressions with side-effects are allowed in the debug statement. These include not only methods with side-effects but also increment (++) and decrement (--) operators and various forms of assignment expressions (e.g., =, +=, etc.). Thus, the debug statement can also be used to assign a value to a variable, or mutate the state of an object.

//@ debug x = x + 1; //@ debug aList.add(y);

However, a model variable cannot be assigned to, nor can its state be mutated by using the debug statement, as its value is given by a represents clause (see section 8.4 Represents Clauses).

There is no restriction on the type of expression allowed in the debug statement.

Tools should allow debug statements to be turned on or off easily. Thus programmers should not count on debug statements being executed. For example, if one needs to assign to a ghost variable, the proper way to do it is to use a set-statement (see section 13.4.2 Set Statements), which would execute even if debug statements are not being executed.

13.4.6 Hence By Statements

The syntax of the hence_by statement is as follows.

hence-by-statement ::= hence-by-keyword predicate ; hence-by-keyword ::= hence_by | hence_by_redundantly

The hence_by statement is used to record reasoning when writing a proof by intermittent assertions. It would normally be used between two assert statements (see section 13.3 Assert Statements) or between two assume statements (see section 13.4.1 Assume Statements).

[[[Needs example.]]]