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.
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.
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}; **/
}
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!
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.
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 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.
/** check x >= 0; **/
The next section explains how assertion violation can be handled to improve the robustness of the software.
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.
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.
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:
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.