Abstract
An “observational” specification language for abstract data types is one that allows only observable aspects of a type to be specified. An observational sublanguage of first-order logic must not contain equations between values of hidden sorts. It is shown that in such a sublanguage the behaviour of a simple counter data type cannot be finitely specified. This implies that more than first-order logic is needed for a useful observational specification language, and that more than first-order logic or a stronger proof rule than previously proposed is needed to work with nonstandard “behavioural” semantics of specifications.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Jon Barwise, editor. Handbook of Mathematical Logic. Number 90 in Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam et al., 1977.
Klaus Bothe. A comparative study of abstract data type concepts. Elektronische Informationsverarbeitung und Kybernetik, 17:237–257, 1981.
V. Giarratana, F. Gimona, and U. Montanari. Observability concepts in abstract data type specification. In A. Mazurkiewicz, editor, Mathematical Foundations of Computer Science 1976, number 45 in LNCS, pages 576–587, Gdańsk, Poland, 1976. Springer.
John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading, Mass. et al., 1979.
Marek Karpinski, editor. Foundations of Computation Theory, number 158 in LNCS, Borgholm, Sweden, 1983. Springer.
Barbara H. Liskov and Stephen N. Zilles. Specification techniques for data abstractions. IEEE Transactions on Software Engineering, SE-1:7–19, 1975.
G. Mirkowska and A. Salwicki. Algorithmic Logic. D. Reidel, Dordrecht et al., 1987. Also published by PWN—Polish Scientific Publishers, Warsaw.
D. L. Parnas. A technique for software module specification with examples. Communications of the ACM, 15:330–336, 1972.
Horst Reichel. Behavioural validity of conditional equations in abstract data types. In Contributions to General Algebra 3. Proceedings ... 1984, pages 301–324. Hölder-Pichler-Tempsky, Vienna, 1985. Also published by B. G. Teubner, Stuttgart.
Oliver Schoett. Ein Modulkonzept in der Theorie Abstrakter Datentypen. Bericht 81, Fachbereich Informatik, Universität Hamburg, August 1981.
Oliver Schoett. Behavioural correctness of data representations. Science of Computer Programming, 14:43–57, 1990.
Donald Sannella and Andrzej Tarlecki. On observational equivalence and algebraic specification. Journal of Computer and System Sciences, 34:150–178, 1987.
Donald Sannella and Andrzej Tarlecki. Toward formal development of programs from algebraic specifications: Implementations revisited. Acta Informatica, 25:233–281, 1988.
Donald Sannella and Martin Wirsing. A kernel language for algebraic specification and implementation. Internal Report CSR-131-83, Department of Computer Science, University of Edinburgh, September 1983. Extended Abstract in [Kar83], p. 413–427.
J. W. Thatcher, E. G. Wagner, and J. B. Wright. Data type specification: Parameterization and the power of specification techniques. ACM Transactions on Programming Languages and Systems, 4:711–732, 1982.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schoett, O. (1991). An observational subset of first-order logic cannot specify the behaviour of a counter (extended abstract). In: Choffrut, C., Jantzen, M. (eds) STACS 91. STACS 1991. Lecture Notes in Computer Science, vol 480. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0020824
Download citation
DOI: https://doi.org/10.1007/BFb0020824
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53709-0
Online ISBN: 978-3-540-47002-1
eBook Packages: Springer Book Archive