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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 1985
Accession Number
ADA327436

Entities

People

  • Carolyn Talcott
  • Ian A. Mason

Organizations

  • Stanford University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Artificial Intelligence
  • Cancellation
  • Cells
  • Computational Science
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Information Processing
  • Language
  • Lisp Programming Language
  • Mathematical Models
  • Models
  • Notation
  • Programming Languages

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Parallel and Distributed Computing.