1 Assertions

In this chapter the kinds of assertions that are possible in Jass will be described. The description of the syntax will be illustrated by brief examples of the class Buffer and done in the form of grammatical rules.

The chapter is subdivided into the following parts:

• The assertion language
• Preconditions and postconditions: 'require' and 'ensure'
• The class invariant: 'invariant'
• The loop invariant and the loop variant: 'invariant' and 'variant'
• The check-statement: check'
• The rescue-block: 'rescue' and the retry-statement: 'retry'
• How assertions are checked
• Comments in assertions

2 The assertion language

Jass supports different kind of assertions which are used to specify different properties of a java class. All assertions must appear in formal comments and have a introducing keyword which specifies the kind of the assertion. In the most cases than follows a list of boolean expressions which describe the allowed states. The boolean expressions can contain variables and method calls.

To allow arbitrary boolean expressions and method calls is dangerous. This will "... open the gates of the declarative city to the applicative hordes." Assertions describe states but should not modify them.

Jass does restrict the usage of expressions and methods: The expressions must be pure declarative, so no side effects like assignment and instance creation can be used. Called methods must be free of side effects too.

Example for a simple precondition:

/** require !isFull(); o != null; **/

Attention: After the last boolean expression must appear a semicolon and the comment must be closed through '**/'.

The semicolon connects the assertions like a logical 'and' so that the whole precondition ultimately is nothing but one boolean expression. The semicolon can therefore be used in order to divide the expression into smaller and clearer parts and, if desired, to give each part a label of its own:

/** require [buffer_not_full] !isFull(); 
            [object_is_valid] o != null; **/

The label stands in brackets in front of the assertion part and identifies the assertion in error messages.

The boolean expressions of an assertion are produced through the following EBNF:

BooleanAssertion	::=	( AssertionLabel )? AssertionExpression
AssertionLabel	::=	"[" <IDENTIFIER> "]"

The following table gives an overview about the semantic side conditions of the assertions. See the descriptions of the assertions for a detailed explanation.

kind of assertion	type of expressions	usage of fields and methods	usage of local variables	usage of formal parameters	usage of Old and Result
precondition	boolean	special	not allowed	allowed	not allowed
postcondition	boolean	allowed	not allowed	allowed	allowed
class invariant	boolean	allowed	not allowed	not allowed	not allowed
loop invariant	boolean	allowed	allowed	allowed	not allowed
loop variant	int	allowed	allowed	allowed	not allowed
check	boolean	allowed	allowed	allowed	not allowed

Recursive definitions of assertions are not allowed. This means: A call of the method that declares the assertions in the assertion is forbidden. This is true for indirect recursion too.

3 Forall and exists expressions

With the usage of forall and exists the programmer can express properties that must be valid for all elements of an finite set of assertions or for one element of this set.

Example for a forall expression:

(forall i : {out%buf.length .. in%buf.length-1} # buf[i] != null);

Forall and exists expressions are produced through the following EBNF:

AssertionExpression	::=	( AssertionForAllExistsExpression | AssertionConditionalExpression )
AssertionForAllExistsExpression	::=	( <FORALL> | <EXISTS> ) <IDENTIFIER> ":" ( AssertionFiniteEnumerationCreation | AssertionRangeExpression ) <FORALL_SEP> AssertionExpression
AssertionFiniteEnumerationCreation	::=	"new" Name AssertionArguments
AssertionRangeExpression	::=	"{" AssertionShiftExpression <RANGE> AssertionShiftExpression "}"

4 Preconditions and postconditions: 'require' and 'ensure'

As in Eiffel, for each method of a class in Java a precondition and a postcondition can be stated by the Jass extensions. The precondition is at the beginning of the method body (directly after the opening brace), the postcondition is at the end (before the close brace).

With the precondition the developer can specify the states in which a method may be invoked. To satisfy the precondition is the duty of the caller. The precondition is introduced through the keyword require.

Example for a precondition:

public void addElement (Object o) {
/** require !isFull(); o != null; **/
...
}

The method addElement can only be invoked if the buffer is not full and the formal parameter contains a reference to an valid object that should be inserted. Inserting a null reference is forbidden.

The called methods and used variables in the precondition must be as visible as the method they appear in. This availability rule ensures that the caller will understand the conditions under which the method can be invoked. This implies that local variables can not be used.

In the above examples the method isFull must be declared public to satisfy this condition.

A postcondition specifies the states in which the method should return. To satisfy the postcondition is the duty of the developer of the method. The postcondition is introduced through the keyword ensure.

Example for a postcondition:

public void addElement (Object o) {
...
/** ensure !isEmpty() && contains(o); **/
}

On return of the method addElement the buffer can not be empty and the object to insert should be contained.

The postcondition can contain three special constructs: Old, changeonly and Result. This constructs are explained in the following.

The object state at the begin of the method is stored in the special variable Old. With this variable the developer can specify relations between entry and exit states. For example the monotony of a counter.

Example for the use of Old:

public void addElement (Object o) {
...
/** ensure !isEmpty() && contains(o); Old.count == count-1; **/
}

To store a copy of the object at the begin of the method the developer must implement the method clone without throwing any exception (The interface java.lang.Cloneable must implemented!). Thus the developer decides how a copy is generated. This is a feature not a bug! Objects may reference complex data structures. Only the developer can decide which parts must be copied and which can be shared.

Another special construct is the changeonly keyword followed by a list of attributes. If such a list is specified in a postcondition only the declared attributes are allowed to change their values. Not listed attributes must remain constant. The empty list stands for: change nothing. To check this a copy of the object is generated with the clone method analogous to the Old construct. The attributes are compared with the method equals which can be overwritten by the developer. This is a feature, too! Attributes of array type are handled differently. If the array type is unidimensional the contents are compared with the equals method through a loop. If the array has more than one dimension the whole array is compared for reference equality. This approach follows the equals method for array objects.

Example for the use of changeonly:

public void addElement (Object o) {
...
/** ensure !isEmpty() &&  contains(o); 
           Old.count == count-1; 
           changeonly{count,buffer}; **/

}

Pre- and Postcondition are produced through the following EBNF:

MethodDeclaration	::=	( "public" | "protected" | "private" | "static" | "abstract" | "final" | "native" | "synchronized" | "strictfp" )* ResultType MethodDeclarator ( "throws" NameList )? ( "{" MethodBodyBlock "}" | ";" )
MethodBodyBlock	::=	( RequireClause )? ( BlockStatement )* ( EnsureClause )? ( RescueClause )?
RequireClause	::=	<REQUIRE> ( BooleanAssertion ";" )+ <ASS_END>
EnsureClause	::=	<ENSURE> ( BooleanChangeAssertion ";" )+ <ASS_END>
BooleanAssertion	::=	( AssertionLabel )? AssertionExpression
BooleanChangeAssertion	::=	( <CHANGEONLY> "{" ( ChangeList )? "}" | BooleanAssertion )
ChangeList	::=	FieldReference ( "," FieldReference )*
FieldReference	::=	( "this" "." )? <IDENTIFIER>

5 The class invariant: 'invariant'

In each class a class invariant may be stated. This invariant contains assertions, that, apart from the parameter names, may be defined as in the preconditions of methods. The class invariant begins with the keyword invariant and is stated at the end of the class like a method declaration.

The class invariant is supposed to include all assertions that contain conditions that hold for the whole class and not just for single methods. For instance, with their help the possible state space defined by the arrays can be restricted.

The class invariant could also explicitly be added to each precondition and postcondition. The semantics would be the same, but its intention as an invariant condition could hardly be recognized. Changes of the invariant would imply changes in all pre- and postconditions.

Like a method, the class invariant is declared at the end of the class and it is called by the other methods at the positions in which it is supposed to be checked.

Example for a class invariant:

public class Buffer {
...
/** invariant 0 <= in - out && in - out <= buffer.length; **/
}

No local variables and formal parameters can be used in the class invariant.

The class invariant is checked whenever a method of the class is called or ended. Analogous to the postcondition the end of a method are the return statements and the end of the body. If the assertion expressions of the invariant contain variables that can be changed through other instances Jass warns the developer with a message. In this case the invariant can be invalidated without any error message produced.

The invariant is produced through the following EBNF:

ClassDeclaration	::=	( "abstract" | "final" | "public" | "strictfp" )* UnmodifiedClassDeclaration
UnmodifiedClassDeclaration	::=	"class" <IDENTIFIER> ( "extends" Name )? ( "implements" NameList )? ClassBody
ClassBody	::=	"{" ( ClassBodyDeclaration )* ( ClassInvariantClause )? "}"
ClassInvariantClause	::=	<INVARIANT> ( InvariantAssertion ";" )+ <ASS_END>

6 The loop invariant and the loop variant: 'invariant' and 'variant'

Some kinds of errors are typical for loops:

• The loop does not terminate.
• The loop body is execute once too often or to less.
• Special cases like zero iterations are not handled.

To take the edge of the loops the loop invariant and the loop variant are introduced. Both are declared after the head and before the body of a loop. If, in the following, confusion with the class invariant cannot be excluded by the context, we use the expression "loop invariant". This invariant states an assertion that must be influenced by the execution of the loop, while the variant denotes an integer expression that explicitly has to do this. Two conditions are linked to the variant: first, its value has to be positive all the time, second, this value must decrease every time the loop is repeated. The Jass precompiler checks these conditions; as both conditions cannot be maintained infinitely long, the loop has to terminate.

As loops can only be used within methods their assertions are not directly part of the documentation but they describe the implementation. Therefore, they do not contribute to the contract between developer and user. They do have an important function, however. They can reveal properties of the implementation that cannot be detected at first sight; in particular, the time limitation for loops can be shown. They thereby promote the understanding and help the developer formulate a precise precondition and postcondition or class invariant.

In the case of the forms discussed so far (the integration of assertions in the program code), it was implicitly assumed that the method call terminates and therefore returns to the caller at some point. This point of view is correct if loops are disregarded. With loops the time limitation has to be indicated explicitly, as otherwise the postcondition would never be checked and thus no guarantees as in a contract or in the form of a correctness formula could be given (see Design by contract).

Example for a loop invariant and variant:

   public boolean contains(Object o) {
   /** require o != null; **/
      for (int i = 0; i < buffer.length; i++) 
      /** invariant 0 <= i && i <= buffer.length; **/
      /** variant buffer.length - i **/
         if (buffer[i].equals(o)) return true;
      return false;
  /** ensure changeonly{}; **/    
  }

If both constructs are used the loop invariant must declared before the loop variant. The expression of the variant must be of type int and can not be decorated with a label. There is no semicolon at the end of the variant!

The invariant and variant are produced through the following EBNF:

WhileStatement	::=	"while" "(" Expression ")" AssertionClause
DoStatement	::=	"do" AssertionClause "while" "(" Expression ")" ";"
ForStatement	::=	"for" "(" ( ForInit )? ";" ( Expression )? ";" ( ForUpdate )? ")" AssertionClause
AssertionClause	::=	( InvariantClause )? ( VariantClause )? Statement
InvariantClause	::=	<INVARIANT> ( BooleanAssertion ";" )+ <ASS_END>
VariantClause	::=	<VARIANT> AssertionExpression <ASS_END>

7 The check-statement: 'check'

The check statement is used to state an assertion at any part of the program code of the method body. It shows that at this position the validity of the condition is expected, although the reason for this is not immediately obvious from the program code.

For instance, at some point in the program code let there be the assignment x=y/z. The programmer is sure that at this position z never equals 0. For this reason, he does not want to check this, such a check being superfluous. The reason for a value unequal to 0 may be found at another, more distant, position in the program code, possibly even in another method.

Someone else who looks over the whole code and who cannot recognize the reason immediately, is likely to assume that a mistake has been made or at least that the programming has been done rather sloppily. And even the programmer himself cannot always be aware of every single detail of the whole system and may want to be reminded of this important property. The check-statement formulates it explicitly: check z!=0;. Of course, the check-statement can also be checked during runtime.

Example for a check statement:

/** check x >= 0; **/

The check statement is produced through the following EBNF:

CheckClause

::=

<CHECK> ( BooleanAssertion ";" )+ <ASS_END>

8 The rescue-block: 'rescue' and the retry statement: 'retry'

By stating a rescue-block the integrity of the respective instance can be secured in the case of a violated exception (e.g. by closing files or freeing memory). A detailed description of the aims of its use is given in Violations of the contract: success or failure.

It consists of a sequence of catch-statements which each contain a block with statements that can contain a retry statement.

Example for a rescue block:

   public void add(Object o) {
   /** require [valid_object]    o != null; 
               [buffer_not_full] !full();   **/  ...
   /** ensure ... **/
   /** rescue catch (PreconditionException e) {
                 if (e.label.equals("valid_object")) {
		     o = new DefaultObject(); retry;}
                 else throw e;
              }
  }

This example catches a precondition exception and reinitiates the method call with a reassigned formal parameter. A default object is created and inserted in the buffer if the formal parameter was null. The assertion label is used to distinct between the two possible exceptions.

The rescue construct can only be applied to exception of (sub)type of AssertionException. If no retry statement appears in the block the exception is throw again at the end of the code block.

The check statement is produced through the following EBNF:

RescueClause	::=	<RESCUE> ( RescueCatch )+ ( ";" )? <ASS_END>
RescueCatch	::=	"catch" "(" FormalParameter ")" Block
RetryStatement	::=	<RETRY> ";"

9 How assertions are checked

Each assertion, except for the loop invariant, is a boolean expression the validity of which can be checked in a conditional statement with a preceding negation operator. This negation triggers an exception if the assertion condition is invalid.

The precondition and the postcondition are changed at the beginning and at the end of a method call, respectively. The end of a method call is a return statement or the end of the method body. If an Old construct is used a local variable will be declared at the beginning of the methods body. This variable will be assigned the value produced by the clone method. The changeonly construct uses this mechanism too.

Bertrand Meyer has stated a important principal for the evaluation of assertions:

While the evaluation of an assertion no other assertion should be evaluated.

This means: If the evaluation of an assertion invokes a method that declares an assertion too this second assertion should not be evaluated. Jass does implement a compromise of this principal. If an assertion contains a call to a method of the same class this method is copied in an internal version without any assertion checks. While the evaluation of this assertion the internal version is called. If the internal version calls another method with assertions these will be checked again. Thus the principal is implemented on the first level for internal calls.

The class invariant is translated into a new method which is called from the preconditions and postconditions.

With loops the invariant is checked at the beginning of each run and directly after a conditional statement. A local variable is generated for the variant. It temporarily stores the value at the beginning of a run such that it is possible to check at the end whether its value has decreased and whether it is still positive. However for loops need some extra work to be done.

The check-statement is locally expanded like a macro. A conditional statement for the check of its assertion is directly generated from it.

Jass triggers the following exceptions which are located in the package jass.runtime:

Exception	Is thrown when ...
PreconditionException	... the precondition of a method does not hold.
PostconditionException	... the postcondition of a method does not hold.
InvariantException	... the invariant of a class does not hold.
LoopInvariantException	... the loop invariant for a certain loop iteration does not hold.
LoopVariantException	... the loop variant is not decreased or out of its bounds.
CheckException	... the assertion of a check statement does not hold.
RefinementException	... the class signals a refinement but does not match the refinement requirements.

10 Comments in assertions

Comments in assertions make it easier to understand what semantic constraints are expressed. Java does not support nested comments, so a Jass developer can not write normal Java comments within an assertion. Therefore Jass supports the special comment signs /# and #/ to be used in assertions.

Example of comments in an assertion:

/** require
 /# The buffer must contain space to store the object: #/ !isFull();
 /# Only 'valid' objects can be used: #/ o != null;
**/