On the implementation of at pre

Abstract

The paradigm of design by contract provides a transparent way of specifying object-oriented systems. There exist a number of languages for contractual specification including OCL, JML and Spec#. Nevertheless, there are still a number of research problems concerning this approach. One of them is the implementation of primitive @pre in OCL or equivalently old in JML. Those primitives are used in postconditions to refer to attribute values in states preceding an operation execution. There are a number of implementations of this operators, but all suffer logical and computational problems. In this paper, existing approaches to the implementation of @pre are discussed and a new solution is proposed.