Abstract
We propose a set of algebraic laws for reasoning with sequential imperative programs that use object references like in Java. The theory is based on previous work by adding laws to cope with object references. The incrementality of the algebraic method is fundamental; with a few exceptions, existing laws for copy semantics are entirely reused, as they are not affected by the proposed laws for reference semantics. As an evidence of relative completeness, we show that any program can be transformed, through the use of our laws, to a normal form which simulates it using an explicit heap with copy semantics.
This is a preview of subscription content, log in via an institution to check access.
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
Back, R.J.R., van Wright, J.: Refinement calculus: a systematic introduction. Springer (1998)
Banerjee, A., Naumann, D.: Ownership confinement ensures representation independence for object-oriented programs. J. ACM 52, 894–960 (2005)
Banerjee, A., Naumann, D.A., Rosenberg, S.: Local reasoning for global invariants, part I: Region logic. Journal of the ACM 60, 18:1–18:56 (2013)
Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL, pp. 14–25 (2004)
Berger, M., Honda, K., Yoshida, N.: A logical analysis of aliasing in imperative higher-order functions. SIGPLAN Not. 40(9), 280–293 (2005)
Borba, P., Sampaio, A., Cavalcanti, A., Cornélio, M.: Algebraic reasoning for object-oriented programming. Science of Computer Programming (2004)
Bornat, R.: Proving pointer programs in Hoare logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 102–126. Springer, Heidelberg (2000)
Cornélio, M., Cavalcanti, A., Sampaio, A.: Sound refactorings. Science of Computer Programming (2010)
Hoare, C.A.R., et al.: Laws of programming. Communications of the ACM 30(8) (1987)
Hoare, C.A.R., Staden, S.: In praise of algebra. Formal Aspects of Computing, 423–431 (2012)
Hoare, T., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra and its foundations. J. Log. Algebr. Program. 80(6), 266–296 (2011)
Jifeng, H., Li, X., Liu, Z.: rCOS: A refinement calculus of object systems. Theoretical Computer Science 365(1-2), 109–142 (2006)
Kassios, I.T.: The dynamic frames theory. Formal Aspects of Computing 23, 267–288 (2011)
Kozen, D.: On Hoare logic and Kleene algebra with tests. In: ACM Trans. Comput. Logic. (July 2000)
Lucero, G., Naumann, D., Sampaio, A.: Laws of programming for references, long version (2013), http://www.cs.stevens.edu/~naumann/pub/LuceroNSfull.pdf
Morgan, C.: Programming from specifications. Prentice-Hall, Inc. (1990)
Morris, J.: A general axiom of assignment. In: Broy, M., Schmidt, G. (eds.) Theoretical Foundations of Programming Methodology (1982)
Naumann, D.A., Sampaio, A., Silva, L.: Refactoring and representation independence for class hierarchies. Theoretical Computer Science 433, 60–97 (2012)
O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Computer Science Logic (2001)
Silva, L., A., Sampaio, Z.L.: Laws of object-orientation with reference semantics. In: IEEE Software Engineering and Formal Methods (2008)
Staton, S.: Completeness for algebraic theories of local state. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 48–63. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Lucero, G., Naumann, D., Sampaio, A. (2013). Laws of Programming for References. In: Shan, Cc. (eds) Programming Languages and Systems. APLAS 2013. Lecture Notes in Computer Science, vol 8301. Springer, Cham. https://doi.org/10.1007/978-3-319-03542-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-03542-0_9
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-03541-3
Online ISBN: 978-3-319-03542-0
eBook Packages: Computer ScienceComputer Science (R0)