Jass - News

1 Current and Future Work

Currently we are improving Jass 2.x in the sense of fixing bugs and improving the source code. The source code should be more readable by better structuring and documenting it.

As our second task, the trace assertion feature is completely redesigned and improved. This work was mainly done by Mark Br�kens as his mastersthesis. This new Trace Assertion feature will bring up a different language for traces, so that the current trace-language is not supported any longer. To get an overview of this work have a look at the jassda chapter. There you will also find a link to the jassda homepage

With Jass 3 we are switching to [http://www.jmlspecs.org/]JML as the assertion language - work is in progress. Many of the "standard" assertion features are similar to what Jass provides. But the handling of interfaces, abstract classes and the feature of model variables is much more expressive than that what Jass currently supports. Instead of developing new language extensions we could benefit from switching to a language that is much more elaborated by much more people. Vice versa we could provide the Trace Assertions as extension of JML.

2 Actual Information

This section makes the files NEWS and BUGS of the current Jass distribution available via the Web.

2.1 Changes (NEWS)

jass-2.0.13

jass-2.0.12

Since September 2004:

jass-2.0.11

jass-2.0.10

jass-2.0.9

jass-2.0.8

jass-2.0.7

jass-2.0.6

jass-2.0.5:

jass-2.0.4:

jass-2.0.3:

jass-2.0.2:

jass-2.0.1:

jass-2:

2.2 Known Bugs (BUGS)

Bug:
Not possible to refer to nonstatic methods from within static assertion
Problem:
It is not possible to refer to any nonstatic methods from within an assertion in a static method, even if the nonstatic methods are explicitly on an instance of the class. For instance, the following static method in class Moogle:
Example:
   public static void cactaur(Moogle cait_sith) {
      /** require cait_sith.kupo(); **/
      ...
   }
fails when kupo() is a non-static method of Moogle, even though it's being called on an instance of the class.

Bug:
JassDoc does not work with Java2 SDK/JRE 1.4
Problem:
SUN changed some doclet classes that we derive from
Workaround:
Use the -tag option of javadoc in 1.4. See the example.xml

Bug:
internal Jass methods missing
Message:
Method jassInternal_xxx not found
Occurence:
Compiler
Problem:
If a method 'm' is called within an assertion, Jass calls an internal version of this method: 'jassInternal_m'. Jass creates internal versions of all methods who appear at the assertions of a class. Unfortunately Jass does not take into account yet that assertions may refer to external methods as well.
Example:
public class C {
  public boolean m(){..}
}

public class D {
	C c;
	
  /** invariant c.m(); **/
}
C.jassInternal_m() does not exists!
Workaround:
To lead Jass to create the necessary internal methods, insert dummy conditions into the external class which refer to the affected methods. The above example works with: 
public class C {
  public boolean m(){..}
	/** invariant m() = m(); **/
}

Bug:
Jass creates Java code which may not be reached
Message:
Statement not reached
Occurence:
Compiler
Problem:
Jass inserts code at the exit points of a method (end of method / return statements). This code may not be reached.
Example:
while(true)
{
	... // something
}
jass post condition
Workaround:
Use a dummy statement or a dummy variable to outwit the java mechanism to detect unreachable code

Bug:
Anonymous and method scoped classes can not contain assertions.
Problem:
Assertions in anonymous and method scoped classes are simply ignored.

Bug:
Inner classes can only be handled at first level.
Problem:
A declaration like 
public class Outer {
   public class Test {
      public class Test2 {
      }
   }
}
can not be handled. ReflectVisitor and OutputVisitor have no problem to deal with this! The only problem is the name look up of the NameAnalysis ...

Bug:
Constructors of Inner classes can't be handled.
Problem:
idebughc.ServletLogOutput contains an inner class DummyServletContext with no constructor, therefore the default constructor should be just 
  DummyServletContext() { super(); }
Since no constructor was explicitly specified, Jass introduces one but it has signature: 
  public ServletLogOutput$DummyServletContext()

Bug:
Some constructs are not analysed.
Problem:
Not parsed and analysed are:
The Jass Page - printer friendly - last update 08/07/07
online version at http://csd.informatik.uni-oldenburg.de/~jass