Memories of S-Expressions Proving Properties of Lisp-Like Programs That Destructively Alter Memory,

Abstract
In this paper we present a mathematical model called a memory structure, and define a computation theory over such structures. This computation theory provides a semantics for first-order, lexically scoped Lisp-like languages and we use this as a basis for expressing and proving properties of a variety of programs that destructively alter the contents of memory. Since we have chosen to work in a Lisp-like world, our subject matter is particularly relevant to the Lisp programmer. The main example in this paper is a proof of the correctness of the Robson copying algorithm. This algorithm copies possibly cyclic Lisp style S-expressions using bounded storage and illustrates how destructive memory operations can be used to write fast efficient programs.

This publication has 0 references indexed in Scilit: