AJML 3.0 Readme

The full list of resolved issues in 3.0 can be found here.

Common AJML release 3.0 (August 10, 2011)

Notable Changes

Model fields support

There is now a support to the use of model fields along with JML represents clauses in specification and runtime verification.
Here is an example:

public class Timer {
  private long sec = 0;
  //@ public model long min;
  //@ private represents min = sec / 60;

  //@ ensures \result == min;
  public long getMin() { return sec / 60; }
  // ...
}

Model methods support

There is now a support to the use of model methods in JML specification and runtime verification.
Here is an example:

public class ModelMethod1 {
  int val = 10;

  //@ public pure model int val1() { return val; } 

  //@ requires x > val1();
  public void m1(int x) {}
}

Quantifiers support through model methods

JML allows one to write specifications using quantifiers like forall and exists.
Here is an example:

public interface BoundedStackInteface {
	
   //@ public model instance Object [] theStack;
   //@ public instance represents size = theStack.length;

   //@ public instance invariant theStack != null;
                          
   /*@ public instance invariant 
     @         (\forall int i; 0 <= i && i < theStack.length;
     @                         theStack[i] != null);
     @*/
	
   // other methods...
}

However, the ajmlc 3.0 and prior versions do not support JML quantifiers yet, such as the above forall example. But, we can emulate a forall quantifier using JML model methods.
See the modified version of the previous example:

public interface BoundedStackInteface {
	
   //@ public model instance Object [] theStack;
   //@ public instance represents size = theStack.length;

   //@ public instance invariant theStack != null;
   //@ public instance invariant this.forAllNonNullStack();
	
   /*@  public pure model boolean forAllNonNullStack() {
	 @   boolean isNonNull = true;
	 @   for( int i = 0; 0 <= i && i < theStack.length; i++){
	 @     if(theStack[i] == null) {
	 @       isNonNull = false;
	 @     }
	 @   }
	 @   return isNonNull;
	 @  }   
	 @*/

     // other methods...
}

Runtime verification on client and supplier sites is the default

Since the runtime verification on client site came to fix fundamental problems of conventional runtime verification techniques, including jmlc and previous versions of ajmlc, it is default now on the AJML common tools. Runtime verification on both client and supplier sites being the default is useful if a client is added to a program and it is not compiled against the interface specifications. Hence, the new added client will be checked at least using the old approach on runtime verification in which the runtime checks are in the supplier classes.

Since runtime verification on both client and supplier sites is the default mode now, we have added the following command to disable runtime checking on client site:

At command-line:
usage: org.jmlspecs.jmlrac.Main [option]* [--help] 
options:
  ...
  --noCallSiteInstrumentation, -b:        Disable call site instrumentation and runtime verification [false]

At the AJML ANT Task:
< target name="ajmlc" depends="clean,prepare" description="">
  < ajmlc destdir="${dest.dir}" srcdir="${src.dir}" classpathref="classpath" source="false" ajweaver="ajc" 
    nocallsiteinstrumenation="false" onlycallsiteinstrumenation="false" verbose="true" fork="false">
  < /ajmlc>
< /target>

Note: The above command replace the old one used until version 2.4. In ajmlc version 2.4 or prior versions, the call site option is not the default.

At command-line:
usage: org.jmlspecs.jmlrac.Main [option]* [--help] 
options:
  ...
  --callSiteInstrumentation, -b:        Enable call site instrumentation and runtime verification [false]

At the AJML ANT Task:
< target name="ajmlc" depends="clean,prepare" description="">
  < ajmlc destdir="${dest.dir}" srcdir="${src.dir}" classpathref="classpath" source="false" ajweaver="ajc" 
    callsiteinstrumenation="false" onlycallsiteinstrumenation="false" verbose="true" fork="false">
  < /ajmlc>
< /target>