Observational implementation of algebraic specifications (Q911245)

An observational approach to the construction of implementations of algebraic specifications is presented. Based on the theory of observational specifications an implementation relation is defined which formalizes the intuitive idea that an implementation is correct if it produces correct observable output. To be useful in practice proof theoretic criteria for observational implementations are provided and a proof technique (called ``context induction'') for the verification of implementation relations is presented. As an example an abstract specification of (the algebraic semantics of) a small imperative programming language is implemented by a state oriented specification of the language. In order to support the modular construction of implementations the approach is extended to parameterized observational specifications. Based on the notion of observable parameter context a proof theoretic criterion for parameterized observational implementations is presented and it is shown that under appropriate conditions observational implementations compose horizontally. The given implementation criteria are applied to examples.