zbMATH — the first resource for mathematics

Behavioural and abstractor specifications. (English) Zbl 0853.68130
Summary: In the literature, one can distinguish two main approaches to the definition of observational semantics of algebraic specifications. On one hand, observational semantics is defined using a notion of observational satisfaction for the axioms of the specifications and, on the other hand, one can define observational semantics by abstraction with respect to an observational equivalence relation between algebras.
In this paper, we present an analysis and a comparative study of the different approaches in a more general framework which subsumes the observational case. The distinction between the different observational concepts is reflected by our notions of behavioural specification and abstractor specification. We provide necessary and sufficient conditions for the semantical equivalence of both kinds of specifications and we show that behavioural specifications can be characterized by an abstractor construction and, vice versa, abstractor specifications can be characterized in terms of behavioural specifications. Hence, there exists a duality between both concepts which allows to express each one by the other. We also study the relationships to fully abstract algebras which can be used for a further characterization of behavioural semantics.
Finally, we provide proof-theoretic results which show that behavioural theories of specifications can be reduced to standard theories of some classes of algebras.

68Q65 Abstract data types; algebraic specification
Full Text: DOI