Observational implementation of algebraic specifications
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.
- A systematic study of models of abstract data types
- Algebraic implementation of abstract data types
- scientific article; zbMATH DE number 3888893 (Why is no real title available?)
- scientific article; zbMATH DE number 3898213 (Why is no real title available?)
- scientific article; zbMATH DE number 3936496 (Why is no real title available?)
- scientific article; zbMATH DE number 3978367 (Why is no real title available?)
- scientific article; zbMATH DE number 3714904 (Why is no real title available?)
- scientific article; zbMATH DE number 3754008 (Why is no real title available?)
- scientific article; zbMATH DE number 3765116 (Why is no real title available?)
- scientific article; zbMATH DE number 3774870 (Why is no real title available?)
- scientific article; zbMATH DE number 3776831 (Why is no real title available?)
- scientific article; zbMATH DE number 3784848 (Why is no real title available?)
- scientific article; zbMATH DE number 3529404 (Why is no real title available?)
- scientific article; zbMATH DE number 3995031 (Why is no real title available?)
- scientific article; zbMATH DE number 4113952 (Why is no real title available?)
- On hierarchies of abstract data types
- On the algebraic definition of programming languages
- Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability
- Structured algebraic specifications: A kernel language
- Context induction: A proof principle for behavioural abstractions and algebraic implementations
- A semi-algorithm for algebraic implementation proofs
- Two impossibility theorems on behaviour specification of abstract data types
- Behavioural approaches to algebraic specifications. A comparative study
- scientific article; zbMATH DE number 2038889 (Why is no real title available?)
- Algebraic implementation of abstract data types: a survey of concepts and new compositionality results
- Observational implementations
- Hybrid implementations of algebraic specifications
- Testing can be formal, too
- Observational specifications and the indistinguishability assumption
- Observational purity and encapsulation
This page was built for publication: Observational implementation of algebraic specifications
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q911245)
