View article

A language called ASL for describing structured algebraic specifications is presented. ASL is a declarative higher-order language. It contains constructs for building (possibly infinite) signatures, sets of terms, and sets of formulas as well as constructs embodying primitive operations on algebraic specifications. In particular, ASL includes a very general ‘observability’ operation which can be used to behaviourally abstract from a specification. The expressive power of these operations allows the choice of a simple notion of implementation which is transitive and monotonic. Syntax and two different denotational semantics, a ‘presentation semantics’ and a ‘model class semantics’, are given. The presentation semantics is used for showing the existence of a complete (semiformal) proof system for specifications, whereas the model class semantics is fully abstract with respect to specification expressions. Both semantics …