Accession Number : ADA327436

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

Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Mason, Ian A. ; Talcott, Carolyn L.

PDF Url : ADA327436

Report Date : JUN 1985

Pagination or Media Count : 48

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 :   *COMPUTER PROGRAM VERIFICATION, *STRUCTURED PROGRAMMING, MATHEMATICAL MODELS, ALGORITHMS, COMPUTER COMMUNICATIONS, RANDOM ACCESS COMPUTER STORAGE.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE