Skip to main content

Unifying Theories of Locations

Michael Anthony Smith and Jeremy Gibbons

Abstract

We present a Unifying Theories of Programming (UTP) model of locations, where a location is either shareable or containable depending on whether its value can be dereferenced by a pointer. Our model of locations is similar to previous work on pointers within the UTP; the main difference is that the previous work on pointers only modelled shareable locations. We explain why containable locations are useful, present an outline of our UTP model, and compare it to the existing UTP work. We hope to convince the reader that a general model of pointers within the UTP ought to be able to represent both shareable and containable locations. Here, the contents of contained locations need to be duplicated, whereas the contents of shared locations are referenced.

Address
Dublin
Book Title
Unifying Theories of Programming
Editor
Andrew Butterfield
Month
Sep
Year
2008