Abstract
One can attempt to solve the problem of establishing the correctness of some software w.r.t. a formal specification at the semantical level. For this purpose, the semantics of an algebraic specification should be the class of all algebras which correspond to the correct realizations of the specification. We approach this goal by defining an observational satisfaction relation which is less restrictive than the usual satisfaction relation. The idea is that the validity of an equational axiom should depend on an observational equality, instead of the usual equality. We show that it is not reasonable to expect an observational equality to be a congruence, hence we define an observational algebra as an algebra equipped with an observational equality which is an equivalence relation but not necessarily a congruence. Since terms may represent computations, our notion of observation depends on a set of observable terms. From a careful case study it follows that this requires to take into account the continuations of suspended evaluations of observable terms. The bridge between observations and observational equality is provided by an indistinguishability relation defined on the carriers of an algebra according to the observations. In the general case, this relation is neither transitive nor a congruence.
This work is partially supported by ESPRIT Working Group COMPASS and C.N.R.S. GDR de Programmation.
Chapter PDF
Similar content being viewed by others
Keywords
- Partial Evaluation
- Indistinguishability Relation
- Forgetful Functor
- Satisfaction Relation
- Observational Model
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bernot G., Bidoit M. Proving the correctness of algebraically specified software: Modularity and Observability issues Proceedings of International Conference AMAST, Iowa City, 1991, 139–161
Bernot G., Bidoit M., Knapik T. Observational Approaches in Algebraic Specifications: a Comparative Study Report LIENS-91-6, 1991
Bergstra J.A., Tucker J.V. Initial and Final Algebra Semantics for Data Type Specifications: Two Characterization Theorems. SIAM Journal of Computing, vol 12 (1983), 366–387
van Dieppen N.W.P. Implementation of Modular Algebraic Specifications (Ganzinger H. ed.) ESOP 88, Nancy, March 1988, LNCS 300, 64–78
Ehrig H., Mahr B. Fundamentals of Algebraic Specifications ETACS Monographs on Theoretical Computer Science, Vol 6, Springer-Verlag, 1985
Goguen J.A., Burstall R. Introducing Institutions (Clarke E., Kozen D. eds.) Proceedings of Logic of Programming Workshop, Carnegie Mellon, 1984, LNCS 164, 221–256
Goguen J.A., Burstall R. Institutions: abstract model theory for specification and programming LFCS report ECS-LFCS-90-106 (1990)
Goguen J.A., Meseguer J. Universal Realization, Persistent Interconnection and Implementation of Abstract Modules (Nielsen M., Schmidt E.M. eds.) ICALP, Aarhus, 1982, LNCS 140, 265–281
Goguen J.A., Thatcher J.W., Wagner E.G. An Initial Approach to the Specification, Correctness and Implementation of Abstract Data Types, (Yeh R.T. ed.) Current Trends in Programming Methodology, Vol. 4: Data Structuring, Prentice Hall, 80–149 (1978)
Hennicker R. Context Induction: a Proof Principle for Behavioural Abstractions and Algebraic Implementations Fakultät für Mathematik und Informatik Universität Passau, 1990 (Internal Report MIP-9001)
Kamin S. Final Data Types and Their Specification ACM Transactions on Programming Languages and Systems, Vol 5, No 1, 97–123 (1983)
Knapik T. Sémantique Observationnelle des Spécifications Algébriques: application à la modularité et à l'implémentation Ph. D. thesis in preparation, Université de Paris-Sud, Orsay 1992
Nivela P., Orejas F. Initial Behaviour Semantics for Algebraic Specification (Sannella, Tarlecki eds.) Recent Trends in Data Type Specification, 5th Workshop on Specification of ADT, Gullane, September 1987, LNCS 332, 184–207
Pepper P. On the Correctness of Type Transformations Talk at 2nd Workshop on Theory and Applications of Abstract Data Types, Passau, May 1983
Reichel H. Behavioural Validity of Conditional Equations in Abstract Data Types Contributions to General Algebra 3, Proceedings of the Vienna Conference, June 1984
Sannella D., Tarlecki A. On Observational Equivalence and Algebraic Specification, TapSoft, Berlin 1985, LNCS 185, 308–22
Sannella D., Tarlecki A. Toward Formal Development of Programs from Algebraic Specification Revisited, Acta Informatica 25, 233–281 (1988)
Wand M. Final Algebra Semantics and Data Type Extension Journal of Computer and System Sciences, Vol 19, 27–44 (1979)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bernot, G., Bidoit, M., Knapik, T. (1992). Towards an adequate notion of observation. In: Krieg-Brückner, B. (eds) ESOP '92. ESOP 1992. Lecture Notes in Computer Science, vol 582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55253-7_3
Download citation
DOI: https://doi.org/10.1007/3-540-55253-7_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55253-6
Online ISBN: 978-3-540-46803-5
eBook Packages: Springer Book Archive