Specifying and Checking Method Call Sequences

Our approach is to separate the protocol assertions from the functional assertions. As before, the functional properties are written in the pre and postconditions. However, the protocol properties are written directly as separate annotations in a suitable notation. For this, we extend JML to introduce a new specification clause, called a call sequence clause. The call sequence clause specifies ordering dependencies among method calls. It specifies the allowed sequences of method calls and thus constrains the order in which methods of a class or interface should be called by clients.

The code below shows the applet protocol specified with the newly introduced call sequence clause.

package java.applet;
public class Applet {
  //@ public call_sequence init() : (start() : stop())+ : destroy();
  // member declarations ...
}

We use a regular expression-like notation to express call sequence assertions. In the example, the infix : operator denotes a sequential composition of two call sequence expressions, and the postfix + operator denotes one or more sequential compositions of a call sequence expression. The meanings of the specification should be apparent. The specification describes the life-cycle of applets by stating that init should be called first, followed by some number of alternating calls to start and stop, and destroy should be called last.

In the call sequence assertion, one can also specify alternative calls and nested calls. The following call sequence specification states that the start method should call either the repaint method or the paint(Graphics) method, directly or indirectly; nested calls are enclosed in a pair of curly braces, preceded by the calling method name. The example also shows that an overloaded method can be disambiguated by specifying its formal parameter types, e.g., paint(Graphics).

  init()
    : (start() {repaint() || paint(Graphics)} : stop())+ 
      : destroy()

Syntax

  call-sequence-clause ::= call-sequence-keyword call-sequence-expression ";"
  call-sequence-keyword ::= "call_sequence" | "call_sequence_redundantly"
  call-sequence-expression ::= method-call-sequence-expression
                             | unanry-call-sequence-expression
                             | binary-call-sequence-expression
                             | parenthesized-call-sequence-expression
  method-call-sequence-expression ::= method-signature ["{" call-sequence-expression "}"]
  unary-call-sequence-expression ::=  call-sequence-expression ["*" | "+"]
  binary-call-sequence-expression ::= call-sequence-expression (":" | "||") call-sequence-expression
  parenthesized-call-sequence-expression ::= "(" call-sequence-expression ")"

Semantics