Reasoning with specifications containing method calls and model fields

Abstract

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.