
Accession Number : ADA327436
Title : Memories of SExpressions Proving Properties of LispLike 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 firstorder, lexically scoped Lisplike 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 Lisplike 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 Sexpressions 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