Abstract
This paper shows how to use the transformation of Paterson and Hewitt to improve the memory and operations used in a pointer algorithm. That transformation scheme normally is only of theoretical interest because of the inefficient performance of the transformed function. However we present a method how it can be used to decrease the amount of selective updates in memory while preserving the original runtime performance. This leads to a general transformation framework for the derivation of a class of pointer algorithms.
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
F.L. Bauer, H. Wössner: Algorithmic Language and Program Development, Springer, Berlin, 1984
A. Bijlsma: Calculating with pointers. Science of Computer Programming 12, Elsevier 1989, 191–205
R. Bird: Introduction to Functional Programming using Haskell, 2nd edition, Prentice Hall Press, 1998
R. Bird: Unfolding Pointer Algorithms, to appear in Journal of Functional Programming, available from: http://www.comlab.ox.ac.uk/oucl/work/richard.bird/publications
R. Bornat: Proving pointer programs in Hoare logic. Proceedings of MPC 2000, Ponte de Lima, LNCS 1837, Springer 2000, 102–126
R. Burstall: Some techniques for proving correctness of programs which alter data structures. In B. Meltzer and D. Michie eds, Machine intelligence 7, Edinburgh University Press, 1972, 23–50
M. Butler: Calculational derivation of pointer algorithms from tree operations. Science of Computer Programming 33, Elsevier 1999, 221–260
T. Ehm: Case studies for the derivation of pointer algorithms. to appear
C. A. R. Hoare: Proofs of correctness of data representations. Acta Informatica 1, 1972, 271–281
J.M. Morris: A general axiom of assignment. Theoretical Foundations of Programming Methodology, NATO Advanced Study Institutes Series C Mathematical and Physical Sciences 91, Dordrecht, Reidel, 1981, 25–34
J.M. Morris: Assignment and linked data structures. Theoretical Foundations of Programming Methodology, NATO Advanced Study Institutes Series C Mathematical and Physical Sciences 91, Dordrecht, Reidel, 1981, 35–51
B. Möller: Towards pointer algebra. Science of Computer Programming 21, Elsevier, 1993, 57–90
B. Möller: Calculating with pointer structures. In: R. Bird, L. Meertens (eds.): Algorithmic languages and calculi. Proc. IFIP WG2.1 Working conference, Le Bischenberg. Chapman & Hall 1997, 24–48
B. Möller: Calculating with acyclic and cyclic lists. In A. Jaoua, G. Schmidt (eds.): Relational Methods in Computer Science. Int. Seminar on Relational Methods in Computer Science, Jan 6–10, 1997 in Hammamet. Information Sciences — An International Journal 119, 1999, 135–154
H. Partsch: Specification and transformation of programs. A formal approach to software development. Monographs in Computer Science. Springer, 1990
M.S. Paterson, C.E. Hewitt: Comparative Schematology. Conference on Concurrent Systems and Parallel Computation Project MAC, Woods Hole, Massachuset, USA, 1970
J.C. Reynolds: Intuitionistic reasoning about shared mutable data structures. In: Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of Sir Tony Hoare, Palgrave, 2000
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ehm, T. (2001). Transformational Construction of Correct Pointer Algorithms. In: Bjørner, D., Broy, M., Zamulin, A.V. (eds) Perspectives of System Informatics. PSI 2001. Lecture Notes in Computer Science, vol 2244. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45575-2_13
Download citation
DOI: https://doi.org/10.1007/3-540-45575-2_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43075-9
Online ISBN: 978-3-540-45575-2
eBook Packages: Springer Book Archive