Abstract
In these lectures an observational approach to the semantics of algebraic specification is presented. Observability is defined in a logical way: an algebra is a behavioural model of a specification SP if it satisfies the axioms w.r.t. an observational interpretation of the equality relation.
The advantages of this notion are proof-theoretic ones: the proof system for observational first-order formulae needs just one additional (infinitary) proof schema, the so-called context-induction. The completeness of this proof system for behavioural properties of a specification is shown. Examples for context-induction proofs are given and it is shown how by the theorem of Bidoit & Hennicker context-inductive properties can be proven without explicit use of context-induction.
An ASL-like kernel language for modular behavioural specification is introduced and the correctness of refinements of specifications is studied. Sound and complete proof systems for properties of structured specifications and the validity of behavioural refinements are given. Moreover, behavioural refinement is transitive; the refinement of a subspecification SPO induces a correct refinement of the full specification SP if SP is behaviourally complete w.r.t. SPO.
This work has been partially sponsored by the DFG project SPECTRUM.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
E. Astesiano, G. Reggio, M. Wirsing: Relational specifications and observational semantics. In: I. Gruska, B. Rovan, J. Wiedemann (eds.): Proc. MFCS ’86, Mathematical Foundations of Computer Science, Bratislava, Springer Lecture Notes in Computer Science, 233, 209–217, 1986.
B. Bauer, R. Hennicker: Proving the correctness of algebraic implementations by the ISAR system. In: A. Miola (ed.): Proc. DISCO ’93, International Symposium on Design and Implementation of Symbolic Computation Systems, Springer Lecture Notes in Computer Science, 722–16, 1993.
G. Bernot, M. Bidoit: Proving the correctness of algebraically specified software: modularity and observability issues. Laboratoire d’Informatique de rEcole Normale Supérieure, Paris, Technical Report, LIENS-91-8,1991.
M. Bidoit, R. Hennicker: Proving Behavioural Theorems with Standard First-Order Logic. Submitted for publication, 1994.
M. Broy, M. Wirsing: A modular framework for algebraic specification and implementation. In: J. Diaz, F. Orejas (eds.): Proc. TAPSOFT ’89, Springer Lecture Notes in Computer Science, 351, 42–73, 1989.
C. C. Chang, H. J. Keisler: Model Theory. Amsterdam, North- Holland, 3rd edition, 1990.
S. Garland, J. Guttag: An overview of LP, the Larch Prover. In: Proc. of the Third International Conference on Rewriting Techniques and Applications, Springer Lecture Notes in Computer Science, 355, 137 - 151, 1989.
R. Hennicker: Context induction: a proof principle for behavioural abstractions and algebraic implementations. Formal Aspects of Computing 3 (4), 326- 345, 1991.
R. Milner: Fully abstract models of typed X-calculi. Theoretical Computer Science 4, 1 - 22, 1977.
F. Nicki, R. Hennicker: A behavioural algebraic framework for modular system design with reuse. Ludwig-Maximilians-Universität München, Technical Report 9206, 1992.
F. Orejas, M. P. Nivela: Constraints for behavioural specifications. In: H. Ehrig, K. P. Jantke, F. Orejas, H. Reichel (eds.): Recent trends in Data Type Specifications, Proc. 7th Workshop on Specification of Abstract Data Types, Wusterhausen/Dosse, Springer Lecture Notes in Computer Science, 534, 220-245, 1990.
H. Reichel: Initial restrictions of behaviour. IFIP Working Conference, The Role of Abstract Models in Information Processing, 1985.
D. T. Sannella, A. Tarlecki: On observational equivalence and algebraic specification. Journal Comp, and Sys. Sciences 34, 150 - 178, 1987.
D. T. Sannella, A. Tarlecki: Toward formal development of ML programs: foundations and methodology. In: J. Diaz, F. Orejas (eds.): Proc. TAPSOFT ’89, Springer Lecture Notes in Computer Science, 352, 375-389, 1989.
D. T. Sannella, M. Wirsing. A kernel language for algebraic specifications and implementation. In: M. Karpinski (ed.): Proc. FCT ’83, Springer Lecture Notes in Computer Science 158, 413-427, 1983.
O. Schoett: Data abstraction and the correctness of modular programming. Ph.D. thesis, CST-42-87, Department of Computer Science, Univ. Edinburgh, 1987.
M. Wirsing: Structured algebraic specifications: a kernel language. Theoretical Computer Science 42, 123 - 249, 1986.
M. Wirsing: Algebraic specification. In: J. van Leeuwen (ed.): Handbook of Theoretical Computer Science, Amsterdam, North-Holland, 675 - 788, 1990.
M. Wirsing: Structured specifications: syntax, semantics and proof calculus. In: F. L. Bauer, W. Brauer, H. Schwichtenberg (eds.): Logic and Algebra of Specification, International Summer School Marktoberdorf, 1991, NATO ASI Series F, Vol. 94, Springer, 411 - 442, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hennicker, R., Wirsing, M. (1995). Behavioural Specifications. In: Schwichtenberg, H. (eds) Proof and Computation. NATO ASI Series, vol 139. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-79361-5_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-79361-5_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-79363-9
Online ISBN: 978-3-642-79361-5
eBook Packages: Springer Book Archive