Jass - Documentation

Jass Handbook

1 Jass handbook

The precompiler Jass translates a .jass file to a .java. This file can be compiled with a Java compiler in byte code. The compiler javac from Sun included in JDK 1.2 is reference. The Jass precompiler is used from commandline like javac.

2 The commandline syntax

The following grammar rules specify the commandline.

Start is the start symbol of the grammar and Filename a platform specific file name of the class to compile.

3 Options

The options divide in two groups. Options for the [#translation]translation, called compile options, and [#general]general options. Some compile options may be annotated with a list of [#commands]control commands, called compile controls, that specify the code to generate.

3.1 Compile options

There are three different translation modes and a special mode for interference checks. The modes contract, warning and nothing translate a .jass file to a Java file. The modes will be explained below.

contract (default)

The mode contract represents the understanding of design by contract. A break of the contract will trigger an exception.

warning

The mode warning is for the integration of assertions in existing projects. A break of the contract triggers not an exceptions. A warning message is displayed at the terminal in this case. The rescue construct has no function in this mode.

nothing

In mode nothing no assertions will be translated.

interference

The mode interference is for interference checks of the program. The mode can only be used for classes with main method. After an analysis Jass displays the results of the check. This is the information if an interference is possible and which control flow interferes with which assertion.

A list of compile controls defines which assertions should be translated, if an refinement should be taken in account and if optimization should be done.

3.2 Compile controls

pre

Preconditions will be checked.

post

Postconditions will be checked.

inv

Class invariants will be checked.

loop

Loop variants and invariants will be checked.

check

Check assertions will be checked.

forall

Quantified expressions (forall,exists) will be checked.

refine

A refinement is taken in account.

trace

Trace assertions will be checked.

opt

The destination code (java) will be optimized.

The usage of the compile control list is optional. All controls except the command opt are used by default. The multiple use of controls has no special effects.

Versions 2.0.6 and 2.0.7 of Jass have a bug in parsing the compile control list. These version will only use the first control. The others are ignored!

3.3 General options

With the general options the basic behaviour of the precompiler is determined.

-d <dir>

Output goes to destination directory <dir>. This option must be set if you use .java suffix instead of .jass suffix for your source code files.

-source <release>

Provide source compatibility with specified Java release. If you want to translate source code that uses Java's new assert keyword you must set the option -source 1.4

-quiet

No console output is done.

-normal (default)

Important message are displayed

-verbose

Many message of all system components are displayed. This option is for debugging purpose.

-depend

If the class is a refinement the superclass will be translated too. In later versions this option will translated all necessary classes.

-nodepend (default)

No depending classes will be translated.

-dataflow

Dataflow analysis is done. This option will increase time and space requirements a lot! This option will be activated automatically with the command opt or the mode interference.

-nodataflow (default)

No dataflow analysis is done. Method calls in assertions are not checked for freedom of side effects.

-jassdoc (default)

Userdefined sections for assertions are inserted into existing formal comments. This can be used by your own Doclets, for example jass.util.doc.JassDoc

-htmldoc

Use HTML code to format assertions in existing formal comments.

-nodoc

Do not add any code for assertions to existing formal comments.

If contrary options (e.g. quiet and verbose) are used the last one has priority.

4 Examples

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

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.