TY - GEN
T1 - Laws of programming for references
AU - Lucero, Giovanny
AU - Naumann, David
AU - Sampaio, Augusto
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84893385901
UR - https://www.scopus.com/pages/publications/84893385901#tab=citedBy
U2 - 10.1007/978-3-319-03542-0_9
DO - 10.1007/978-3-319-03542-0_9
M3 - Conference contribution
AN - SCOPUS:84893385901
SN - 9783319035413
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 124
EP - 139
BT - Programming Languages and Systems - 11th Asian Symposium, APLAS 2013, Proceedings
T2 - 11th Asian Symposium on Programming Languages and Systems, APLAS 2013
Y2 - 9 December 2013 through 11 December 2013
ER -