Abstract
A data structure is said to be persistent when any update operation returns a new structure without altering the old version. This paper introduces a new notion of persistence, called semi-persistence, where only ancestors of the most recent version can be accessed or updated. Making a data structure semi-persistent may improve its time and space complexity. This is of particular interest in backtracking algorithms manipulating persistent data structures, where this property is usually satisfied. We propose a proof system to statically check the valid use of semi-persistent data structures. It requires a few annotations from the user and then generates proof obligations that are automatically discharged by a dedicated decision procedure.
Chapter PDF
References
Baker, H.G.: Shallow binding makes functional arrays fast. SIGPLAN Not. 26(8), 145–147 (1991)
Mike Barnett, K., Leino, R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, Springer, Heidelberg (2005)
Benedikt, M., Reps, T.W., Sagiv, S.: A decidable logic for describing linked data structures. In: European Symposium on Programming, pp. 2–19 (1999)
Blanchet, B.: Escape analysis: Correctness proof, implementation and experimental results. In: Symposium on Principles of Programming Languages, pp. 25–37 (1998)
Conchon, S., Contejean, E.: Ergo: A Decision Procedure for Program Verification, http://ergo.lri.fr/
Conchon, S., Filliâtre, J.-C.: A Persistent Union-Find Data Structure. In: ACM SIGPLAN Workshop on ML, Freiburg, Germany (October 2007)
Conchon, S., Filliâtre, J.-C.: Semi-Persistent Data Structures. Research Report 1474, LRI, Université Paris Sud (September 2007), http://www.lri.fr/~filliatr/ftp/publis/spds-rr.pdf
Dijkstra, E.W.: A discipline of programming. Series in Automatic Computation. Prentice Hall Int., Englewood Cliffs (1976)
Driscoll, J.R., Sarnak, N., Sleator, D.D., Tarjan, R.E.: Making Data Structures Persistent. Journal of Computer and System Sciences 38(1), 86–124 (1989)
Filliâtre, J.-C.: The Why verification tool, http://why.lri.fr/
Filliâtre, J.-C., Marché, C.: The Why/Krakatoa/Caduceus Platform for Deductive Program Verification (Tool presentation). In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, Springer, Heidelberg (to appear, 2007)
Hannan, J.: A type-based analysis for stack allocation in functional languages. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol. 983, pp. 172–188. Springer, Heidelberg (1995)
Knuth, D.E.: Dancing links. In: Davies, B.R.J., Woodcock, J. (eds.) Millennial Perspectives in Computer Science, Palgrave, pp. 187–214 (2000)
Morrisett, J.G., Crary, K., Glew, N., Walker, D.: Stack-based typed assembly language. In: Types in Compilation, pp. 28–52 (1998)
Nelson, G.: Verifying reachability invariants of linked structures. In: POPL 1983: Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 38–47. ACM Press, New York (1983)
Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, Cambridge (1998)
Ranise, S., Zarba, C.: A theory of singly-linked lists and its extensible decision procedure. In: SEFM 2006: Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods, Washington, DC, USA, pp. 206–215. IEEE Computer Society, Los Alamitos (2006)
Spalding, F., Walker, D.: Certifying compilation for a language with stack allocation. In: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005), Washington, DC, USA, pp. 407–416. IEEE Computer Society, Los Alamitos (2005)
Tofte, M., Talpin, J.-P.: Implementation of the typed call-by-value lambda-calculus using a stack of regions. In: Symposium on Principles of Programming Languages, pp. 188–201 (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Conchon, S., Filliâtre, JC. (2008). Semi-persistent Data Structures. In: Drossopoulou, S. (eds) Programming Languages and Systems. ESOP 2008. Lecture Notes in Computer Science, vol 4960. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78739-6_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-78739-6_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78738-9
Online ISBN: 978-3-540-78739-6
eBook Packages: Computer ScienceComputer Science (R0)