Programming Languages and Systems (TOPLAS)


Search Issue
enter search term and/or author name


ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 2 Issue 3, July 1980

Managing Reentrant Structures Using Reference Counts
Daniel G. Bobrow
Pages: 269-273
DOI: 10.1145/357103.357104
Automatic storage management requires that one identify storage unreachable by a user's program and return it to free status. One technique maintains a count of the references from user's programs to each cell, since a count of zero implies the...

Chaining Span-Dependent Jump Instructions
Bruce W. Leverett, Thomas G. Szymanski
Pages: 274-289
DOI: 10.1145/357103.357105
The assembled length of a span-dependent jump instruction depends on the distance between the instruction and its target. Such instructions are found on many computers and typically have two forms, long and short. We consider the problem of...

A Coroutine Approach to Parsing
Hanan Samet
Pages: 290-306
DOI: 10.1145/357103.357106
A method is presented for parsing syntactic constructs that are permitted to appear independently anywhere in a program. Some examples include comments, macros, and constructs for conditional compilation. Each such construct is defined by its...

Applicability of Software Validation Techniques to Scientific Programs
W. E. Howden
Pages: 307-320
DOI: 10.1145/357103.357107
Error analysis involves the examination of a collection of programs whose errors are known. Each error is analyzed and validation techniques which would discover the error are identified. The errors that were present in version five of a package...

Derivation of Invariant Assertions During Program Development by Transformation
Manfred Broy, Bernd Krieg-Bruckner
Pages: 321-337
DOI: 10.1145/357103.357108
Two approaches to the development of efficient and correct iterative programs are contrasted: the construction of an iterative program and a proof of its correctness using invariant assertions of loops, and the construction and proof of a...

Synthesis of Resource Invariants for Concurrent Programs
Edmund Clarke, Jr.
Pages: 338-358
DOI: 10.1145/357103.357109
Owicki and Gries have developed a proof system for conditional critical regions. In their system, logically related variables accessed by more than one process are grouped together as resources, and processes...

A Proof System for Communicating Sequential Processes
Krzysztof R. Apt, Nissim Francez, Willem P. de Roever
Pages: 359-385
DOI: 10.1145/357103.357110
An axiomatic proof system is presented for proving partial correctness and absence of deadlock (and failure) of communicating sequential processes. The key (meta) rule introduces cooperation between proofs, a new concept needed to deal with...

A Formal System for Reasoning about Programs Accessing a Relational Database
Marco R. Casanova, Phillip A. Bernstein
Pages: 386-414
DOI: 10.1145/357103.357111
A formal system for proving properties of programs accessing a database is introduced. Proving that a program preserves consistency of the database is one of the possible applications of the system. The formal system is a variant of dynamic...

An Improved Context-Free Recognizer
Susan L. Graham, Michael Harrison and Walter L. Ruzzo
Pages: 415-462
DOI: 10.1145/357103.357112
A new algorithm for recognizing and parsing arbitrary context-free languages is presented, and several new results are given on the computational complexity of these problems. The new algorithm is of both practical and theoretical interest. It...

Corrigendum: “Distributed Termination”
Nissim Francez
Page: 463
DOI: 10.1145/357103.357113