Abstract
An induction principle, called context induction, is presented which is appropriate for the verification of behavioural properties of abstract data types. The usefulness of the proof principle is documented by several applications: the verification of behavioural theorems over a behavioural specification, the verification of behavioural implementations and the verification of “forget-restrict-identify” implementations.
In particular, it is shown that behavioural implementations and “forget-restrict-identify” implementations (under certain assumptions) can be characterised by the same condition on contexts, i.e. (under the given assumptions) both concepts are equivalent. This leads to the suggestion to use context induction as a uniform proof method for correctness proofs of algebraic implementations.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Boyer, R. S. and Moore, J. S.:A Computational Logic Handbook. Academic Press, 1988.
Broy, M., Möller, B., Pepper, P. and Wirsing, M.: Algebraic Implementations Preserve Program Correctness.Science of Computer Programming,7(1), 35–54 (1986).
Broy, M., Pair, C. and Wirsing, M.: A Systematic Study of Models of Abstract Data Types.Theoretical Computer Science,33, 139–174 (1984).
Burstall, R. M.: Proving Properties of Programs by Structural Induction.Computer Journal,12, 41–48 (1969).
Ehrig, H. and Mahr, B.:Fundamentals of Algebraic Specification 1. EATCS Monographs on Theoretical Computer Science, Vo. 6, Springer-Verlag, 1985.
Ehrig, H., Kreowski, H. J., Mahr, B. and Padawitz, P.: Algebraic Implementation of Abstract Data Types.Theoretical Computer Science,20, 209–263 (1982).
Garland, S. J. and Guttag, J. V.: Inductive Methods for Reasoning about Abstract Data Types.Proc. POPL'88, pp. 219–228, 1988.
Giarratana, V., Gimona, F. and Montanari, U.: Observability Concepts in Abstract Data Type Specification. In:Proc. MFCS '76, 5th Int. Symp. on Mathematical Foundations of Computer Science, A. Mazurkiewicz (ed.), Lecture Notes in Computer Science45, Springer-Verlag, pp. 576–587, 1976.
Goguen, J. A. and Meseguer, J.: Completeness of Many-Sorted Equational Logic.ACM SIGPLAN Notices,16(7), 24–32 (1981);17(1), 9–17 (1982).
Hennicker, R.: Context Induction: a Proof Principle for Behavioural Abstractions. In:Proc. DISCO '90, Int. Symp. on Design and Implementation of Symbolic Computation Systems, A. Miola (ed.), Capri, April 1990, Lecture Notes in Computer Science429, Springer-Verlag, pp. 101–110, 1990.
Hennicker, R.: Observational Implementation of Algebraic Specifications.Acta Informatica,28(3), 187–230 (1991).
Hennicker, R.: A Semi-Algorithm for Algebraic Implementation Proofs. Technische Berichte der Fakultät für Mathematik und Informatik, Universität Pasau, MIP-9108, 1991.
Kamin, S.: Final Data Types and Their Specification.ACM TOPLASS,5(1), 97–121 (1983).
Nivela, M a P. and Orejas, F.: Initial Behaviour Semantics for Algebraic Specifications. In:Proc. 5th Workshop on Algebraic Specifications of Abstract Data Types, D. T. Sannella and A. Tarlecki (eds), Lecture Notes in Computer Science332, Springer-Verlag, pp. 184–207, 1988.
Padawitz, P. and Wirsing, M.: Completeness of Many-Sorted Equational Logic Revisited.Bulletin EATCS,24, 88–94 (1984).
Pepper, P., Broy, M., Bauer, F. L., Partsch, H., Dosch, W. and Wirsing, M.: Abstrakte Datentypen: Die algebraische Spezifikation von Rechenstrukturen.Informatik-Spektrum,5, 107–119 (1982).
Reichel, H.: Initial Restrictions of Behaviour.IFIP Working Conference, The role of Abstract Models in Information Processing, 1985.
Sannella, D. T. and Wirsing, M.: Implementation of Parameterized Specifications. In:Proc. ICALP '82, 9th Coll. on Automata, Languages and Programming, M. Nielsen and E. M. Schmidt (eds), Lecture Notes in Computer Science140, Springer-Verlag, pp. 473–488, 1982.
Wand, M.: Final Algebra Semantics and Data Type Extensions.Journal of Computer and System Sciences,19, 27–44 (1979).
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Hennicker, R. Context induction: A proof principle for behavioural abstractions and algebraic implementations. Formal Aspects of Computing 3, 326–345 (1991). https://doi.org/10.1007/BF01642507
Received:
Accepted:
Issue Date:
DOI: https://doi.org/10.1007/BF01642507