Getting Started...
This guide provides a step-by-step example which shows how Modern Jass is used. It is devided into three different sections:- Defining the behviour of a program
- Compiling a program and its contracts
- 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. Themain
-method of the program Bar
requires that the numbers of passed
arguments is even (args.length % 2 == 0
).
1: package foo; 2: 3: import jass.modern.*; 4: 5: public class Bar { 6: 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/Bar.javaThe 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
.
Running
At runtime, contracts are enforced by Modern Jass. This is achived using bytecode instrumentation, so that your program terminates with anAssertionError
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.BarThe
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
.