jContractor Crash Course

Contents

What is jContractor

The Goal of this Tutorial

Writing contracts

  class Stack implements Cloneable {
    private Stack OLD;

    private Vector implementation;

    public Stack () { ... }

    public Stack (Object [] initialContents) { ... }

    public void push (Object o) { ... }

    public Object pop () { ... }

    public Object peek () { ... }

    public void clear () { ... }

    public int size () { ... }

    public Object clone () { ... }

    private int searchStack (Object o) { ... }
  }

Preconditions

  protected boolean push_Precondition (Object o) {
    return o != null;
  }

  private boolean searchStack_Precondition (Object o) {
    return o != null;
  }

  protected boolean Stack_Precondition (Object [] initialContents) {
    return (initialContents != null) && (initialContents.length > 0);
  }

• Contract methods may not have preconditions.
• Native methods may not have preconditions.
• The main(String [] args) method may not have a precondition.
• The precondition for a static method must be static.
• The precondition for a non-static method must not be static.
• The precondition for a non-private method must be protected.
• The precondition for a private method must be private.

Postconditions

  protected boolean push_Postcondition (Object o, Void RESULT) {
    return implementation.contains(o) && (size() == OLD.size() + 1);
  }

  protected boolean size_Postcondition (int RESULT) {
    return RESULT >= 0;
  }

  protected boolean Stack_Postcondition (Object [] initialContents,
                                         Void RESULT) {
    return size() == initialContents.length;
  }

Rules about postcondtions:

• Contract methods may not have postconditions.
• Native methods may not have postconditions.
• The postcondition for a static method must be static.
• The postcondition for a non-static method must not be static.
• The postcondition for a non-private method must be protected.
• The postcondition for a private method must be private.
• Postconditions for constructors cannot refer to OLD.

Invariants

  protected boolean _Invariant () {
    return size() >= 0;
  }

• Invariants are not checked for contract methods.
• Invariants are not checked for static methods.
• Invariants are not checked for native methods.
• Invariants are checked only at the exit of a constructor.
• The _Invariant() method must be protected and non-static.

What happens when a contract is violated?

Separate contract classes

  class Stack_CONTRACT extends Stack {
    private Stack OLD;

    private Vector implementation;

    protected boolean Stack_Postcondition (Object [] initialContents,
                                           Void RESULT) {
      return size() == initialContents.length;
    }

    protected boolean Stack_Precondition (Object [] initialContents) {
      return (initialContents != null) && (initialContents.length > 0);
    }

    protected boolean push_Precondition (Object o) {
      return o != null;
    }

    protected boolean push_Postcondition (Object o, Void RESULT) {
      return implementation.contains(o) && (size() == OLD.size() + 1);
    }

    private int searchStack (Object o) {
      return 0;
    }

    private boolean searchStack_Precondition (Object o) {
      return o != null;
    }

    protected boolean _Invariant () {
      return size() >= 0;
    }
  }

Using contract classes, it is possible to add contracts to classes for which you do not have source code.

When a contract is specified in the non-contract class and in a contract class, the two are logical and-ed together.

Inheritance and interfaces

A subclass method must:

• Accept all input valid to the superclass method.
• Meet all guarantees of the superclass method.

Interfaces may have contracts too (written in contract classes), so contracts can inherit multiply. Contracts from interfaces are logical or-ed with the superclass and subclass contracts in the case of preconditions, and logical-anded in the case of postconditions and invariants, just as you would expect.

Using predicate logic expressions

Running jContractor

  Usage: jContractor [options] class

         jInstrument [options] class

To run your program with contract checking enabled you need only run jContractor and pass the name of the class to run as a command line argument. Any command line arguments that appear after the class name are passed to the main(String [] args) method of that class. For example, if you want to run the class MyProgram.class (which is somewhere on the class path), use a command like this:

$ java jContractor MyProgram

 $ java  jInstrument ./MyProgram.class
 $ java MyProgram

Controlling the instrumentation level

$ java jContractor -pre * -post bar.* -all bar.FooBar Foo

1. none - No contracts are checked.
2. pre - Preconditions are checked.
3. post - Preconditions and postconditions are checked.
4. all - Preconditions, postconditions, and invariants.

  $ cat Foo.instr
  *              pre
  bar.*          post
  bar.FooBar     all

  $ java jContractor -f Foo.instr Foo

Removing contract methods from compiled classes

Here's a simple example:

  $ javac Test.java
  $ javap Test       
  Compiled from Test.java
  public class Test extends java.lang.Object {
      public Test();
      public void foo();
      protected boolean foo_Precondition();
      protected boolean foo_Postcondition(java.lang.Void);
      protected boolean _Invariant();
      public static void main(java.lang.String[]);
  }
  $ java jInstrument -s Test.class
  $ javap Test       
  Compiled from Test.java
  public class Test extends java.lang.Object {
      public Test();
      public void foo();
      public static void main(java.lang.String[]);
  }

1. none - No contracts are removed.
2. pre - Postconditions and invariants are removed.
3. post - Invariants are removed.
4. all - All contracts are removed.