Specifying and Checking Method Call Sequences

Summary

In a pre and postconditions-style specification, it is difficult to specify the allowed sequences of method calls, referred to as protocols. The protocols are essential properties of reusable object-oriented classes and application frameworks, and the approaches based on the pre and postconditions, such as design by contracts (DBC) and formal behavioral interface specification languages (BISL), are being accepted as a practical and effective tool for describing precise interfaces of (reusable) program modules. We propose a simple extension to the Java Modeling Language (JML), a BISL for Java, to specify protocol properties in an intuitive and concise manner. The key idea of our approach is to separate protocol properties from functional properties written in pre and postconditions and to specify them in a regular expression-like notation. The semantics of our extension is formally defined and provides a foundation for implementing runtime checks.

Approach

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

The call sequence clause can appear in a type (class or interface) declaration and has the following form.
  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

A call sequence specification constrains a program by specifying the allowed histories of all executions of the program, where the history of a sequential program execution is a sequence of method calls and returns. A call sequence specification, therefore, denotes a set of allowed histories of program executions. A program execution satisfies a call specification if the history of the program execution is contained in the set of sequences denoted by the specification. A loose semantics is used for runtime checks in that all the methods not appearing in the specification are ignored.

Implementation

An extended JML compiler that supports the call sequence clause is available from Yoonsik Cheon's Software Download Page.

Documentation

For Local Developers


Last modified: $Id: callseq.html,v 1.4 2007/06/15 21:53:50 cheon Exp $