Reasoning with specifications containing method calls and model fields

Abstract

Allowing abstraction in program specifications increases modularity and comprehensibility and is as important in specifications as it is in the program itself; two such abstraction mechanisms are method invocations and model fields. However, method invocations do not map neatly into the first-order logics that are often used for assuring the correctness of specifications. One problem is translating specifications in a way that acknowledges the potential for exceptional behavior. Furthermore, translating model fields into verification conditions exposes the non-trivial interactions between frame conditions and the model representations. The ESC/Java2 tool has been able to achieve 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. © JOT, 2005.