Unifying Theories of Locations

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.