Reasoning with specifications containing method calls and model fields.
David R. Cok · The Journal of Object Technology · 2005
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.