Linear Maps

Abstract:

Verification of large programs is impossible without proof techniques that allow local reasoning and information hiding. In this paper, we resurrect, extend and modernize an old approach to this problem first considered in the context of the programming language Euclid, developed in the 70s. The central idea is that rather than modeling the heap as a single total function from addresses (integers) to integers, we model the heap as a collection of partial functions with disjoint domains. We call each such partial function a linear map. Programmers may select objects from linear maps, update linear maps or transfer addresses and their contents from one linear map to another. Programmers may also declare new linear map variables, pass linear maps as arguments to procedures and nest one linear map within another. The program logic prevents any of these operations from duplicating locations and thereby breaking the key heap representation invariant: the domains of all linear maps remain disjoint. Linear maps facilitate modular reasoning because programs that use them are also able to use the simple, classical frame and anti-frame rules to preserve information about heap state across procedure calls. We illustrate our approach through examples, prove that our verification rules are sound, and show that operations on linear maps may be erased and replaced by equivalent operations on a single, global heap.