J.J. Homing Editor
Abstract Data Types and Software Validation
John V. Guttag, Ellis Horowitz, and DavidR. Musser University of Southern California
A data abstraction can be naturally specified using algebraic axioms. The virtue of these axioms is that they permit a representation-independent formal specification of a data type. An example is given which shows how to employ algebraic axioms at successive levels of implementation. The major thrust of the paper is twofold. First, it is shown how theuse of algebraic axiomatizations can simplify the process of proving the correctness of an implementation of an abstract data type. Second, semi-automatic tools are described which can be used both to automate such proofs of correctness and to derive an immediate implementation from the axioms. This implementation allows for limited testing of programs at design time, before a conventionalimplementation is accomplished. Key Words and Phrases: abstract data type, correctness proof, data type, data structure, specification, software specification CR Categories: 4.34, 5.24
Corrigendum. Programming Languages
David Gries, An Exercise in Proving Parallel Programs Correct, Comm. A C M 20, 12 (Dec. 1977), 921-930. Dr. Leslie Lamport detected what appeared to be a methodological mistake inthe proof of the on-the-fly garbage collector. The assignment atleastgray(m[t].left) of the Collector (see the algorithm labeled (3.6) on page 925) contains references to the two shared variables m[z].lefi and m[m[t].leftl.color, and this clearly violates the restriction (2.10) found on page 923. The problem is not a methodological error but a missing footnote. The statement atleastgray(m[t].left)in (3.6) does have a footnote number 3 attached to it, and an earlier version of the paper [Springer Lecture Notes in Computer Science 46, 1976, 57-81] contained the footnote
This should be written as "t:= m[t].left; atleastgray(t)'" where t is a local variable. Since the mutator never tests the color of a node and only grays a node using also atleastgray, the single statementatleastgray(m[t].left) is equivalent under parallel operation to this sequence of two operations.
1. Introduction The key problem in the design and validation of large software systems is reducing the amount of cornPermission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the ACM copyright notice and the title of...