Reasoning with specifications containing method calls and model fields

By: David R. Cok


Method invocations and model fields are used to write abstract, modular, comprehensible program specifications. Unfortunately, method invocations do not map neatly into the first-order logics that are often used for assuring the correctness of specifications. Similarly, translating model fields into verification conditions uncovers non-trivial interactions between frame conditions and the model representations. The ESC/Java2 tool supports a practical translation of method invocations and model fields within the design constraints of its parent tool, ESC/Java. Furthermore, the techniques used are applicable to other specification constructs such as generalized quantifiers.

Cite as:

David R. Cok, “Reasoning with specifications containing method calls and model fields”, Journal of Object Technology, Volume 4, no. 8 (October 2005), pp. 77-103, doi:10.5381/jot.2005.4.8.a4.

PDF | HTML | DOI | BiBTeX | Tweet this | Post to CiteULike | Share on LinkedIn