Abstract
We present a formalism for specification of pointer datastructures and programs operating on them, based on temporal specifications of dynamic algebras. It is an extension of .rst-order logic with temporal branching-time combinators. The use of this formalism is illustrated by examples.We also propose a Hoare-style calculus for verification of while-programs (operating on pointers) against specifications written in the proposed formalism, which is sound and complete in the sense of Cook.
This research was supported by the Polish Scientific Research Committee (KBN) under grant 8T11C 01515.
Chapter PDF
Similar content being viewed by others
Keywords
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
K.R. Apt. Ten years of Hoare’s logic: A survey — part I. ACM Transactions on Programming Languages and Systems, 3(4):431–483, Oct. 1981.
H. Bickel and W. Struckmann. The Hoare logic of data types. Technical Report 95-04, Technische Universität Braunschweig, Deutschland, 1995.
R. Cartwright and D. Oppen. The logic of aliasing. Acta Inf., 15:365–384, 1981.
T.H. Cormen, C.E. Leiserson, and R. L. Rivest. Introduction to Algorithms. The MIT Press, 1990.
G. Costa and G. Reggio. Specification of abstract dynamic-data types: A temporal approach. Theoretical Comput. Sci., 173(2):513–554, 1997.
O.-J. Dahl. Verifiable Programming. Prentice Hall, 1992.
H. Ehrig and B. Mahr. Fundamentals of Algebraic Specificaton 1. Number 6 in EATCS MTCS. Springer-Verlag, 1985.
Y. Feng and J. Liu. A temporal approach to algebraic specifications. In J. C. M. Baeten and J. W. Klop, editors, CONCUR’90: Theories of Concurrency: Unification and Extension, number 458 in LNCS, pages 216–229. Springer-Verlag, 1990.
C.A.R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12:576–583, 1969.
C.A.R. Hoare and H. Jifeng. A trace model for pointers and objects. In ECOOP’99, number 1628 in LNCS, pages 1–18. Springer-Verlag, 1999.
T.M.V. Janssen and P. van Emde Boas. On the proper treatment of referencing, dereferencing and assignment. In G. Goos and J. Hartmanis, editors, Automata, Languages and Programming, number 52 in LNCS, pages 282–300. Springer-Verlag, 1977.
N. Klarlund and M.I. Schwartzbach. Graph types. In Proceedings of the 20th Symposium on Principles of Programming Languages, pages 196–205. ACM, 1993.
N. Klarlund and M.I. Schwartzbach. Graphs and decidable transductions based on edge constraints. In S. Tison, editor, Trees in Algebra and Programming — CAAP’94. Proceedings, number 787 in LNCS, pages 187–201. Springer-Verlag, 1994.
M. Kubica. Temporal-style speci.cations of pointer data-structures. Technical Report TR 02-03 (268), Institute of Informatics, Warsaw University, 2002.
J.M. Spivey. The Z notation, A Reference Manual. Second edition. Prentice-Hall, 1992.
A. Szatlas. Towards the temporal approach to abstract data types. Fundamenta Informaticae, XI:49–63, 1988.
W. Thomas. Languages, automata, and logic. In Handbook of Formal Languages, volume 3, chapter 7. Springer-Verlag, 1997.
M. Wirsing. Algebraic specifications. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 13, pages 676–788. Elsevier, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg 2003
About this paper
Cite this paper
Kubica, M. (2003). A Temporal Approach to Specification and Verification of Pointer Data-Structures. In: Pezzè, M. (eds) Fundamental Approaches to Software Engineering. FASE 2003. Lecture Notes in Computer Science, vol 2621. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36578-8_17
Download citation
DOI: https://doi.org/10.1007/3-540-36578-8_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00899-6
Online ISBN: 978-3-540-36578-5
eBook Packages: Springer Book Archive