Overview
Modern Jass implements a new concept to bring Design by Contract to Java. Basically,
it uses Java 5 annotation to specify contracts, the Pluggable Annotation Processing API to
validate contracts, and the Bytecode Instrumentation API to enforce contracts.
Outline
Modern Jass is new and somehow cool, because:- it offers a rich feature set,
- it integrates seamless into every IDE and build process,
- it is easy to maintain.
How to specify contracts?
As mentioned above, Modern Jass uses Java 5 annotations to specify contracts. Put in simple words, annotations are 'type-safe' comments that are used to add arbitary meta-information to a Java program. A short introduction to annotations is provided by Sun as part of the lanuage guide.Modern Jass defines several annotation types that allow to define the behaviour of a Java program. For instance, there is the
@Invariant
-annotation which allows to define
an invariant. Other annotation in Modern Jass are:
@Pre/@Post
- Pre/Post-conditions@SpecCase
- A full method specification (normal and exceptional behaviour)@Also
- A container for multiple specifications@NonNull
- A flyweight annotation to state that a reference is not null@Min
- A flyweight annotation to define the lower bound of a numerical value- ...
How to validate contracts?
Usually, a contract is Java code which evaluates to a boolean. For instance, the value of the attribute
expr, @Invariant(expr = "foo != null")
, must be interpreted as Java code. Firstly, it must
be ensured that the expression evaluates to a boolean, and secondly the expression must be valid Java code.
Validating contracts is to performs these steps.
Since Java 6, the pluggable annotation processing API exists. It allows to write plug-ins for the Java compiler
that processes annotations. In combination with the Compiler API, this API is utilised to validate contracts.
The advantage here is that both APIs are part of the standard Java edition, making Modern Jass being seamless
integrated into every IDE and build process. The screenshots below shows how Modern Jass integrates into the
Eclipe IDE. In this case, the post-condition tries to access the return value of a void
method.
How to enforce contracts?
The previous two sections have shown how contracts are specified and how contracts are validated. Still,
to have any effect, contracts must be enforced when a program is executed. Enforcing contracts is to evalute
the specified assertions at runtime, and to abort execution as soon as an assertion is violated.
Modern Jass uses the Bytecode Instrumentation API to enforce contracts. During contract validation, bytecode
is generated for each assertions. These bytecodes are patched into the program while it is loaded into the
virtual machine. Since Java 5, bytecode instrumentation is supported natively. The Java virtual machine switch
-javaagent:<agent_lib>
is used to install a bytecode instrumentation agent.
The screenshot below shows a violated pre-condition, and how the execution of a Java program has been
aborted.