The Jass Page

Tour - Introduction to Jass

[English] printer friendly version

1 The Example: Buffer

The following pages refer to an examples called Buffer which is included in the Jass examples directory. You can view a HTML version of the code. Note that the examples of the tour contain more assertions than the buffer example. This Tour does not cover the Trace-Assertion feature of Jass 2.x, which are described in the documentation only.

2 General Layout of the 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 the keyword is followed by a list of boolean expressions which describe the allowed states. The boolean expressions can contain variables and method calls. The expression 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. Quantifed expressions like forall and exists can used to make statements about sets.

Example of a simple precondition:

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

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

For the most kind of assertions there can be declared a label that identifies the assertion in error messages:

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

The next sections of the tour describes the different kind of assertions with code examples. The tour is ended with an introduction in the commandline syntax of the precompiler.

3 Pre- and Postconditions of Methods

With a 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 checked at the begin of the methods body. The precondition must be declared at the begin of the method body with the introducing keyword require.

Example for a precondition:

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

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

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 checked at all normal return points. These are all return statements and the end of the method body. The postcondition must be declared at the end of the method body with the introducing keyword ensure.

Example for a postcondition:

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

In a postcondition the return value of the method can be accessed with the special variable Result. 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); count == Old.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. If java.lang.Cloneable is not implemented, Old can not be used.

Another special construct is the changeonly keyword followed by a list a attributes. If such a list is specified in a postcondition only the declared attributes are allowed to change there 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 analogously to the Old construct. The attributes are compared with the method equals which can be overwritten through the developer. This is a feature too! Attributes of array type are handled differently. Look at the [Link Name="assert2">complete description of the postcondition[/Link] to learn about this.

Example for the use of changeonly:

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

4 Class Invariant

A class invariant specifies the global state of a class. It expresses restrictions and relationships of the attributs. The class invariant is declared with the introducing keyword invariant and stands at the end of the class body. 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.

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!

5 Loop Variant and Invariant

Some kinds of errors are typical for loops:

To take the edge off the loops the loop invariant and the loop variant are introduced. Both are declared after the head and before the body of a loop.

The loop invariant starts with the keyword invariant and specifies a condition that must be satisfied at the begin of the loop, after every iteration and when the loop has terminated. This is used to express global properties of the loop like the range of the loop variable.

The loop variant has the introducing keyword variant and declares an integer expression that is decreased with every loop iteration but never below zero. Thus the loop variant guaranties the termination of the loop.

Example:

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!

6 Check Statement

The check statement is introduced by the keyword check and can appear wherever a normal statement can stand. When the execution reaches the check statement the condition is checked and if its not valid an exception is thrown.

Example:

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

The next section explains how assertion violation can be handled to improve the robustness of the software.

7 Rescue and Retry

To handle assertion exceptions jass supports a special construct the rescue block. At the end of the method body (behind the postcondition) the user can specify assertion exceptions that should be caught and code blocks that should be executed then. The indicating keyword is rescue. A special keyword retry can be used in the rescue blocks to reinitiate the method call.

Example:

   
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.

8 The jass precompiler

Jass supports a bunch of options to allow a flexible integration of the 'design by contract' into new or existing projects. A class annotated with Jass assertions must be contained in a file with extension '.jass' (or with extension '.java' if a destination directory was specified). The precompiler produces a valid Java class source file with the extension '.java' from the Jass file . This file must be compiled with a Java compiler to get the runtime behaviour specified through design by contract.

The following example demonstrates the simplest invocation of the precompiler (from the Jass main directory):

java jass.Jass jass/examples/Buffer.jass

This produces a file Buffer.java with can be compiled through:

javac examples\Buffer.jass

There are four compilation modes:

contract (default mode)
The produced java file behaves like specified through design by contract. An assertion violation triggers an exception.
warning
An assertion violation triggers not an exception but produces an error message on the terminal (via System.out!). This mode is for a first integration in an existing project with minimal side effects.
nothing
The Jass file is converted to a Java file with no changes in runtime behaviour. This is only a copy process.
interference
This initiates an interference check and does not produce any files.

With the commandline

java jass.Jass -warning jass/examples/Buffer.jass

Jass generates a Java file that produces an error message not an exception when an assertion is violated.

The compilation modes contract and warning can be annotated with compilation controls. The compilation controls decide which kind of assertions are handled and if optimizations should be done. The commandline

java jass.Jass -contract[pre,post,forall] jass/examples/Buffer.jass

produces an output that contains only code for pre- and postcondition checks. The forall and exists expressions are checked trough loops. If the forall control is dropped this expressions are assumed to be true. See the complete documentation for a full description of the controls.