Software Download
Yoonsik Cheon | HOME


JET | JML4c | UTJML | BibPHP | JML

UTJML Overview | Download | Documentation

Call Sequence Clause
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 ")"
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. [more]
API Specifications

Browse the API specifications of the UTJML implementation.

Technical Papers

Last modified: $Id: doc.php,v 1.1 2007/06/15 21:16:09 cheon Exp $