Abstract
We now consider how the material in the preceding chapters must be adapted when we take a behavioural view of specifications, whereby the “behaviour” of an algebra is fully determined by the results delivered by term evaluation. However, only results of certain observable sorts can be directly observed, with two algebras being behaviourally equivalent with respect to the observable sorts if evaluating terms of observable sort always produces the same result in both algebras. This is the essential idea behind data abstraction: we encapsulate a data type together with operations to be used by a client, hiding the actual data representation and any representation-level operations. Then different representations that exhibit the same behaviour can be used interchangeably. Arguably, specifications should not distinguish between algebras that are behaviourally equivalent, which may be ensured by explicitly closing the class of models of a specification under behavioural equivalence. An alternative is to relax the interpretation of equality in sentences so that indistinguishable values of non-observable sorts are regarded as equal.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Sannella, D., Tarlecki, A. (2011). Behavioural specifications. In: Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17336-3_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-17336-3_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17335-6
Online ISBN: 978-3-642-17336-3
eBook Packages: Computer ScienceComputer Science (R0)