The Jass Page


[English] printer friendly version

1 Copyright

Jass is copyrighted in 1999-2005 by the Correct System Design Group , Department of Computing Science at Carl von Ossietzky University of Oldenburg, Germany.

1.1 GNU General Public License

The program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License (GPL) as published by the Free Software Foundation. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

2 Obtaining Jass

To get the software fill out the form below. You must supply a valid email address, which will be used to send you the download URL. All other fields are optional. The email address will only be used for sending the download URL - we will not give it to any third person and will not use it for anything else.

Where did you hear about Jass?
Web Search Engine
Your paper
From a friend
Archive Type: installer (executable jar-archive)
archive only (extract with jar-tool)

3 Jass Package

3.1 Installation

The Jass distribution comes as a Java archive (.jar). To use Jass you have to unpack it. You can unpack the file using the jar tool that is included in the JDK.

Since version 2.0.13 we also provide an executable installer. Just execute the file via (double-)click or via java -jar jass-installer-<version>.jar

3.2 Distribution

Current versions of the Jass distribution archiv contain the following files (and directories):

The .jar-archiv containing the (ready-to-run) Jass precompiler
The .jar-archiv containing classes, that are needed by the Jass-generated Java classes at runtime.
Warning: When using Trace-Assertions you will have to use the jass.jar archiv even at runtime!
Documentation as .jar-archiv
The source files of the Jass precompiler and the runtime classes as .jar-archiv
jass/examples and examples.xml
A directory containing example files and an Ant project file to build it.
The GNU General Public License (GPL) and the GNU Lesser General Public License (LGPL)
Textfiles containing latest information about changes and known bugs.

3.3 Requirements

To use Jass, including the Trace-Assertion feature, at least a Java 2 (JDK 1.2) version is needed.

4 Getting Started

Jass is a pre-compiler. It reads sourcefiles with the suffix '.jass'. A Jass sourcefile is a Java sourcefile where you can insert assertions within Java comments. Jass comes as a jar-archive (jass.jar). To use Jass you need to perform three steps:

At all three steps your classpath must include the Jass archive (jass.jar). (If you are not using the Trace-Assertions feature the jass-rt.jar archiv will be enough for the last step)

The filenames which Jass creates follow a name pattern. If you pre-compile a file named 'someFile.jass' Jass creates

Jass may create some more files if certain dependencies exist (See compiler message 'Compiling file ...'). However all auxilary files got the prefix 'JassTA' (TA: Trace Assertion).

4.1 Example

To run the example 'Factorial.jass' of the directory 'jass/examples/traceAssertion/' type (for Win32-systems):

java -classpath jass.jar;. jass.Jass jass\examples\traceAssertion\Factorial.jass

javac -classpath jass.jar;. jass\examples\traceAssertion\ jass\examples\traceAssertion\JassTA_Factorial*.java

java -classpath jass.jar;. jass.examples.traceAssertion.Factorial

Since Jass version 2.0.12 the Trace Assertion feature is disabled by default. So you have to use the following commandline instead of the first to get the same effect:

java -classpath jass.jar;. jass.Jass -contract [pre,post,inv,loop,check,forall,trace] jass\examples\traceAssertion\Factorial.jass

A full description of commandline syntax of the Jass precompiler can be found at the Jass Handbook.

4.2 Commandline Help

To get help for Jass type java -jar jass.jar or java -jar jass.jar -help