Multiple behaviors

So far our method specifications have been simple sequences of clauses: pre-, frame- and post-conditions. But as methods become more complex it is helpful to separate the method specification into multiple specification cases, which can be specified as different behaviors.

Each behavior is a simple sequence of clauses, with its own preconditions, postconditions, etc. The specification can consist of multiple behaviors, connected by the keyword also. For example,

// openjml --esc T_MultipleBehaviors1.java
public class T_MultipleBehaviors1 {
  //@  requires c >= a && c >= b;
  //@  ensures \result == c;
  //@ also
  //@  requires b >= a && b >= c;
  //@  ensures \result == b;
  //@ also
  //@  requires a >= b && a >= c;
  //@  ensures \result == a;
  //@ pure
  public int max(int a, int b, int c) {
    return a >= b ? ( c >=  a ? c : a) : (c >= b ? c : b);
  }
}

The specification here is a bit more verbose than the code, but it separates out the cases a bit more readably than the code does. Furthermore, by writing the goal of the method in two different ways, an erroneous exchange of ‘a’ for ‘b’ or ‘<’ for ‘>’ is readily caught by OpenJML.

There are a few points to note:

  • There is no order to the behaviors; they can be written in any order that is understandable.
  • Every behavior applies on its own and must hold by itself — there is no if-then-else relationship or ordering among them. If a behavior’s preconditions hold, then its postconditions must hold, independent of what any other behavior says.
  • The effective precondition for each behavior is the conjunction (with &&) of the preconditions for that behavior. The effective precondition for the combination of multiple behaviors is the disjunction (with |) of the effective preconditions of the individual behaviors. Consequently, at the point where such a method is called, at least one, but by no means necessarily all, of the behaviors must have an effective precondition that is true.

In our example, if a, b, and c are all equal, then the precondiition (requires clause) of each of the three behaviors is true. So the postconditions of each of the behaviors must also be true. Fortunately they all agree in that case.

As an experiment, this example introduces a mistake in one behavior:

// openjml --esc T_MultipleBehaviors2.java
public class T_MultipleBehaviors2 {
  //@  requires c >= a && c >= a;
  //@  ensures \result == c;
  //@ also
  //@  requires b >= a && b >= c;
  //@  ensures \result == b;
  //@ also
  //@  requires a >= b && a >= c;
  //@  ensures \result == a;
  //@ pure
  public int max(int a, int b, int c) {
    return a >= b ? ( c >=  a ? c : a) : (c >= b ? c : b);
  }
}

which yields this result

T_MultipleBehaviors2.java:13: verify: The prover cannot establish an assertion (Postcondition: T_MultipleBehaviors2.java:4:) in method max
    return a >= b ? ( c >=  a ? c : a) : (c >= b ? c : b);
    ^
T_MultipleBehaviors2.java:4: verify: Associated declaration: T_MultipleBehaviors2.java:13:
  //@  ensures \result == c;
       ^
2 verification failures

The verification failure message points to the first behavior’s postcondition, on line 4, which narrows our debugging to the relationship between that behavior and the code. A little inspection shows a typo at the end of the first behavior’s precondition, on line 3.

Separating normal from exceptional behaviors

A very common use of multiple behaviors is to separate normal execution from exceptions. For example,

// openjml --esc --nullable-by-default T_MultipleBehaviors3.java
public class T_MultipleBehaviors3 {

    //@  requires a != null;
    //@  requires 0 <= i <= j <= a.length;
    //@  ensures true;
    //@  signals (Exception e) false;
    //@ also
    //@  requires a == null || !(0 <= i <= j <= a.length);
    //@  signals_only IllegalArgumentException;
    //@  ensures false;
    public void inrange(int[] a, int i, int j) { 
        if (a == null) throw new IllegalArgumentException();
        if (i < 0 || j < i || a.length < j) throw new IllegalArgumentException();
        return;
    }
}

The code in this example does some parameter validation checks. If the checks fail an exception is thrown. The method could go on to do something useful, but for this example, it just returns. There are then two behaviors.

  • In the normal case the arguments satisfy the checks and the method just returns normally; that is the first behavior — the ensures postcondition is true (which could be omitted entirely), which just states that the method is allowed (but not required) to return normally; the signals postcondition is false, which states that under these preconditions, the method is not allowed to throw an exception.
  • The second behavior is the exceptional case. Here one or the other of the argument validation checks fails. In this case, the postcondition is ensures false, which means that the method is not allowed to return normally; the default, omitted, signals true clause says that an exception is allowed; the signals_only clause says that if there is an exception it must be an IllegalArgumentException (the only one listed).

We could even separate out two kinds of exceptions:

// openjml --esc T_MultipleBehaviors4.java
public class T_MultipleBehaviors4 {

    //@  requires a != null;
    //@  requires 0 <= i <= j <= a.length;
    //@  ensures true;
    //@  signals (Exception e) false;
    //@ also
    //@  requires a == null || !(0 <= i <= j <= a.length);
    //@  signals_only NullPointerException, ArrayIndexOutOfBoundsException;
    //@  ensures false;
    public void inrange(int[] a, int i, int j) { 
        if (a == null) throw new NullPointerException();
        if (i < 0 || j < i || a.length < j) throw new ArrayIndexOutOfBoundsException();
        return;
    }
}

Now the signals_only clause allows the two kinds of exceptions, although the specification does not say when each one is thrown. We could go to one more level of specification detail to stipulate that each exception is thrown just when the appropriate argument validation check fails. Try specifying that as an exercise. There is a question though: what if both checks fail? Should the specification state which exception is thrown in preference to the other? If it does specify that, then it is constraining the implementation, perhaps overly so. However, if it does not, and both checks fail, then the specification would say that the method should throw both exceptions, which is impossible.

Specialized behaviors

The normal and exceptional behaviors illustrated in the previous section are very common, so much so that they have specialized syntax: normal_behavior and exceptional_behavior. We can rewrite the previous example as

// openjml --esc T_MultipleBehaviors5.java
public class T_MultipleBehaviors5 {

    //@ public normal_behavior
    //@  requires a != null;
    //@  requires 0 <= i <= j <= a.length;
    //@ also public exceptional_behavior
    //@  requires a == null || !(0 <= i <= j <= a.length);
    //@  signals_only NullPointerException, ArrayIndexOutOfBoundsException;
    public void inrange(int[] a, int i, int j) { 
        if (a == null) throw new NullPointerException();
        if (i < 0 || j < i || a.length < j) throw new ArrayIndexOutOfBoundsException();
        return;
    }
}

The normal_behavior heading implies that no exception is allowed (which is equivalent to specifying signals false); the exceptional_behavior heading says that normal termination is not allowed (ensures false). A behavior that is neither of these is a simple behavior, which is the default when there is no heading.

One other point: any one of the behavior keywords needs a visibility keyword; almost always, as in the example above, the visibility is the same as the method. The absence of a visibility modifier means package visibility, just as in Java the absence of a visibility modifier would on the method declaration. However, if there is no specialized behavior keyword, then there is no place for the visibility keyword; in that case, the visibility is the same as the visibility of the method.

Summary of specification cases

To summarize, a method may have multiple specification cases.

  • They are separated/connected by the also keyword.
  • Each specification case consists of an optional heading followed by a series of method specification clauses
  • There are four styles of headings. Here V is a visibility modifier: one of public, protected, private, or absent (meaning package visibility)
    • The most general: V behavior
    • Normal exit only: V normal_behavior
    • Exit by exception only: V exceptional_behavior
    • The most common: no heading, which means V behavior with the visibility V being the same as the method’s visibility

Nested clause groups

We will just mention an advanced topic here: nested clauses groups within a method specification. For details see the JML Reference Manual. Here is an example:

  requires P1;
  ensures Q1;
  {|
     requires P2;
     ensures Q2;
  also
     requires P3;
     ensures Q3;
  |}

which is a less repetitious representation of the equivalent

  requires P1;
  requires P2;
  ensures Q1;
  ensures Q2;
also
  requires P1;
  requires P3;
  ensures Q1;
  ensures Q3;

Multiple Method Behavior Problem Set