Getting Started...

This guide provides a step-by-step example which shows how Modern Jass is used. It is devided into three different sections:
  1. Defining the behviour of a program
  2. Compiling a program and its contracts
  3. Running a program so that its contracts are enforced

Defining behaviour

Defining behaviour is to add contracts to a Java program. In this example, a very simple example is taken. The main-method of the program Bar requires that the numbers of passed arguments is even (args.length % 2 == 0).
 1: package foo;
 3: import jass.modern.*;
 5: public class Bar {
 7: 	@Pre("args.length % 2 == 0")
 8: 	public static void main(String[] args){
 9: 		System.out.println("Hello, " + args.length);
10: 	}
11: }
In line 7, the @Pre-annotation is used which value is a valid Java expression. The semantics is that this expression is going to checked at runtime before the method is executed. However, before a contract can be executed, it must be validated (this the same as compiling Java code).
In the following section we will see how validation of contracts works, and what happens if a contract is not valid.

Compiling / Validating contracts

Modern Jass validates contract while the Java compiler (javac) works. Because Modern Jass uses the annotation processing facilities, it participates in the compilation process, and can validate contracts. The command presented below is all it takes to (a) validate contracts and (b) compile the Java program.
/>javac -cp .:jass.modern.core-20070519.jar foo/
The result is a file foo/Bar.class which is created by the compiler and (optinally) a file called _contracts.jar which is created by Modern Jass.
In case a contract can not be validated successfully, a compile error occurrs. Such a compiler error is created by Modern Jass and presented in the same way a javac-compile error is presented. For instance, when the pre-condition in above example refers to an unknown variable, a contract compile error occurs.

In this case the pre-condition refers to a variable called foo which can not be resolved in the scope of the method main.


At runtime, contracts are enforced by Modern Jass. This is achived using bytecode instrumentation, so that your program terminates with an AssertionError if an assertion is not met.
In order to run your program "contract-protected" invoke the following command:
/>java -javaagent:jass.modern.core-20070519.jar foo.Bar
The javaagent-switch will tell the Java virtual machine to instrument the bytecode of the program with contracts before it is executed.
The pre-condition of the program, states that an even number of parameter must be passed to the program. In the screenshot below, the program is called with an odd number (three) of parameters which causes a PreConditionException.

Modern Jass... a Design by Contract™ implementation for Java™ which uses Java 5 Annotations, the Pluggable Annotation Processing API, the Compiler API, and the Bytecode Instrumentation API



Documents related to my master's thesis Logo