Correct realizations of interface constraints with OCL

Abstract

We present an OCL-like formal notation for interface constraints, called ICL, suited to describe the required observable behavior of any correct interface implementation (provided by some class). The semantics of the ICL notation is defined by a translation to the observational logic institution. For specifying constraints on classes we use a subset of OCL to express invariants and pre- and post-conditions on operations. The semantics of the OCL expressions is defined by a translation into an algebraic specification. Using these semantic foundations we introduce a formal correctness notion for implementation relations between interfaces and classes and we show how to prove implementation correctness by using observational proof techniques.