Tipos abstracto datos

6. Farber, D.J., and Larson, K,C. The structure of a distributed computing system--the communication system. Proc. Symp. Computer-Communications Networks and Traffic, Polytechnic Inst. of Brooklyn, Brooklyn, N.Y., April 1972, pp. 21-27. 7. Fultz, G.L. Adaptive routing techniques for message switching computer communication networks. Ph.D. Th., UCLA-ENG-7252, U. of California, Los Angeles, July1972. 8. Gerla, M. The design of store- and forward (S/F) networks for computer communication. Ph.D. Th., UCLA-ENG-7319, U. of California, Los Angeles, 1973. 9. Harary, F. Graph Theory. Addison-Wesley, Reading, Mass., 1969. 10. Metcalfe, R.M. Packet Communication. Ph.D. Th., Harvard, Proj. Mac Tech. Rep. No. 114, M.I.T., Cambridge, Mass., Dec. 1973. II. Metcalfe, R.M., and Boggs, D.R., Ethernet:Distributed packet switching for local computer networks. Comm. ACM 19, 7 (July 1976), 395-404. 12. McQuillan, J.M. Adaptive routing algorithms for distributed computer networks. Ph.D. Th., Harvard, BBN Rep. 2831, May 1974; available as AD781467, N.T.I.S., Springfield, Va. 13. Paoletti, L.M. AUTODIN. In Computer Communication Networks, R.L. Grimsdale and F.F. Kuo, Eds. (Proc. NATO Advanced StudyInst. Comptr. Comm. Networks, Sussex, U.K., Sept. 1973), Noordoff Int. Publ., Leyden, 1975. 14. Roberts, L.G., and Wessler, B.D. The ARPA computer network. In Computer Communication Networks, N. Abramson and F. Kuo, Eds., Prentice-Hall, Englewood Cliffs, N.J., 1972.

Programming Languages

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...