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
2 The commandline syntax
|Start||::=||( ( CompileOptions )? ( GeneralOptions )* (<FILENAME>)+ ) <EOF>|
|CompileOptions||::=||( ( "-contract" | "-warning" ) ( CompileControls )? )|
|CompileControls||::=||"[" ( "pre" | "post" | "inv" | "loop" | "check" | "forall" | "refine" | "trace" | "opt" )* "]"|
Start is the start symbol of the grammar and Filename a platform specific file name of the class to compile.
The options divide in two groups. Options for the translation, called compile options, and general options. Some compile options may be annotated with a list of control commands, called compile controls, that specify the code to generate.
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
- contract (default)
- The mode contract represents the understanding of design by contract. A break of the contract will trigger an exception.
- 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
rescueconstruct has no function in this mode.
- In mode nothing no assertions will be translated.
- The mode interference is for interference
checks of the program. The mode can only be used for classes with
mainmethod. 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.
- Preconditions will be checked.
- Postconditions will be checked.
- Class invariants will be checked.
- Loop variants and invariants will be checked.
- Check assertions will be checked.
- Quantified expressions (forall,exists) will be checked.
- A refinement is taken in account.
- Trace assertions will be checked.
- 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!
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
.javasuffix instead of
.jasssuffix 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
- No console output is done.
- -normal (default)
- Important message are displayed
- Many message of all system components are displayed. This option is for debugging purpose.
- 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 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
- Use HTML code to format assertions in existing formal comments.
- 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.
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
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]
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.