Laws of programming for references

Giovanny Lucero, David Naumann, Augusto Sampaio

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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.

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 11th Asian Symposium, APLAS 2013, Proceedings
Pages124-139
Number of pages16
DOIs
StatePublished - 2013
Event11th Asian Symposium on Programming Languages and Systems, APLAS 2013 - Melbourne, VIC, Australia
Duration: 9 Dec 201311 Dec 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8301 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference11th Asian Symposium on Programming Languages and Systems, APLAS 2013
Country/TerritoryAustralia
CityMelbourne, VIC
Period9/12/1311/12/13

Fingerprint

Dive into the research topics of 'Laws of programming for references'. Together they form a unique fingerprint.

Cite this