Accession Number:
ADA327436
Title:
Memories of S-Expressions Proving Properties of Lisp-Like Programs That Destructively Alter Memory,
Descriptive Note:
Corporate Author:
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Personal Author(s):
Report Date:
1985-06-01
Pagination or Media Count:
48.0
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.
Descriptors:
Subject Categories:
- Computer Programming and Software