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