The Next Generation

Easy access to old, current and return values are partly implemented. It uses the following new parameterized classes:

  public class Old<T>
  {
    public T value;
    private String m_expression;
    public Old(String expression)
    {
      m_expression = expression;
    }
  }

  public class Current<T>
  {
    public T value;
    private String m_expression;
    public Current(String expression)
    {
      m_expression = expression;
    }
  }

  public class Result<T>
  {
    public T value;
  }

In the contracts you declare local variables of these types to get access to the target object's state, e.g. member variable values or method return values. Each declaration defines an expression that must be valid to execute in the context of the target method the contract is written for, and it must return a value of the type that the local variable is defining. The returned values are stored in the value member of the local variable.
If a variable of type Old is declared, it's value member will contain the return value of the expression that was given to the constructor, as it was before the contracted method was executed.
If a variable of type Current is declared, it's value member will contain the return value of the expression that was given to the constructor, as it is when the contract is executed.
If a variable of type Result is declared, it's value member will contain the return value of the contracted method.
Old and Result declarations are not allowed in pre conditions.
Primitive types are auto boxed.
Note that it is unnecessary to parameterize the local variables if typed access is not necessary, e.g. if only equals is used.

Here is an example:

  public class IntegerStack
  {
    private LinkedList<Integer> m_values = new LinkedList<Integer>();
    public void push(Integer i)
    {
      m_values.add(i, 0);
    }
    public Integer pop()
    {
      return m_values.remove(0);
    }
    public Integer top()
    {
      return m_values.get(0);
    }
    public int size()
    {
      return m_values.size();
    }
  }

  public class IntegerStackContract
  {
    public void post_push(Integer i)
    {
      int currentTop = new Current("top()").value.intValue();
      assert currentTop == i.intValue();
      int oldSize = new Old<Integer>("size()").value.intValue();
      int currentSize = new Current<Integer>("size()").value.intValue();
      assert oldSize == currentSize - 1;
    }
    public void pre_pop()
    {
      int currentSize = new Current<Integer>("size()").value.intValue();
      assert currentSize >= 1;
    }
    public void post_pop()
    {
      Integer oldTop = new Old<Integer>("top()").value;
      Integer result = new Result<Integer>().value;
      assert oldTop.equals(result);
      int oldSize = new Old<Integer>("size()").value.intValue();
      int currentSize = new Current<Integer>("size()").value.intValue();
      assert oldSize == currentSize + 1;
    }
  }

C4J will instrument both the contract and the target class during class loading. The pop method and it's contracts from above will be instrumented in to this:

    public Integer pop()
    {
      Object o0 = size();
      Object o1 = top().clone();
      Object o2 = size().clone();
      c4jContractRef.pre_pop(o0);
      Integer result = m_values.remove(0);
      Object o3 = size();
      c4jContractRef.post_pop(o1, result, o2, o3);
      return result;
    }
    public void pre_pop(Object arg0)
    {
      int currentSize = ((Integer)arg0).intValue();
      assert currentSize >= 1;
    }
    public void post_pop(Object arg0, Object arg1, Object arg2, Object arg3)
    {
      Integer oldTop = (Integer)arg0;
      Integer result = (Integer)arg1;
      assert oldTop.equals(result);
      int oldSize = ((Integer)arg2).intValue();
      int currentSize = ((Integer)arg3).intValue();
      assert oldSize == currentSize + 1;
    }
  }

It is also possible to get access to the target object's member variables, by just passing in the member variable name in the constructors, e.g.
LinkedList<Integer> oldValues = new Old<LinkedList<Integer>>("m_values").value;

All values accessed using Old objects must implement java.lang.Cloneable, regardless of whether they are return values from queries or member variables. This is to avoid the problem when it's the content of a variable that is modified in a method call rather than the reference.

By declaring old, current, or result variables in this way in the contract's method context, recursion and methods calling other methods are automatically supported.
Even multi threading is supported if the target class' method is externally synchronized.

C4J 3 RC1 should come out some time during November or December -06.
Update! It's not gonna happen any time soon I'm afraid, I've simply got too much at my hands currently. Hopefully my employer realizes what they would gain by allowing me to work on C4J as a 20%-project!