Abstraction and verification in Alphard: defining and specifying iteration and generators

ABSTRACT

The Alphard “form” provides the programmer with a great deal of control over the implementation of abstract data types. In this paper the abstraction techniques are extended from simple data representation and function definition to the iteration statement, the most important point of interaction between data and the control structure of the language itself. A means of specializing Alphard's loops to operate on abstract entities without explicit dependence on the representation of those entities is introduced. Specification and verification techniques that allow the properties of the generators for such iterations to be expressed in the form of proof rules are developed. Results are obtained that for common special cases of these loops are essentially identical to the corresponding constructs in other languages. A means of showing that a generator will terminate is also provided.

REFERENCES

• 1: Dahl, O.-J., and Hoare, C.A.R. Hierarchical program structures. In Structured Programming, O.-J. Dahl, E.W. Dijkstra, and C.A.R. Hoare, Academic Press, New York, 1972, pp. 175-220.
• 2: Hoare, C.A.R. A note on the for statement. BIT 12 (1972), 334-341.
• 3: Hoare, C.A.R. Proof of correctness of data representations. Acta lnformatica 1 ,4 (1972), 271-281.
• 4: Hoare, C.A.R., and Wirth, N. An axiomatic definition of the programming language Pascal. Acta lnformatica 2 ,4 (1973), 335- 355.
• 5: Igarashi, S., London, R.L., and Luckham, D.C. Automatic program verification I: a logical basis and its implementation. Acta lnformatica 4, 2 (1975), 145-182.
• 6: Kathleen Jensen , Niklaus Wirth, Pascal-User Manual and Report, Springer-Verlag New York, Inc., Secaucus, NJ, 1975
• 7: Katz, S., and Manna, Z. A closer look at termination. Acta Informatica 5, 4 (1975), 333-352.
• 8: London, R.L., Shaw, M., and Wulf, W.A. Abstraction and verification in Alphard: a symbol table example. Tech. Reports, Inform. Sci. Inst., U. of Southern California, Marina del Rey, Calif., and Carnegie-Mellon U., Pittsburgh, Pa., 1976.
• 9: David C. Luckham , Norihisa Suzuki, Automatic program verification IV: proof of termination within a weak logic of programs., Stanford University, Stanford, CA, 1975
• 10: John McCarthy, LISP 1.5 Programmer's Manual, The MIT Press, 1962
• 11: Newell, A., Tonge, F., Feigenbaum, E.A., Green, B .F. Jr., and Mealy, G.H. Information Processing Language-V Manual. Prentice- Hall, Englewood Cliffs, N.J., Sec. Ed. 1964.
• 12: Shaw, M. Abstraction and verification in Alphard: design and verification of a tree handler. Proc. Fifth Texas Conf. on Computing Systems, 1976, pp. 86-94.
• 13: Shaw, M., Wulf, W.A., and London, R.L. Abstraction and verification in Alphard: Iteration and generators. Tech. Reports, Inform. Sci. Inst., U. of Southern California, Marina del Rey, Calif., and Carnegie-Mellon U., Pittsburgh, Pa., 1976.
• 14: Teitelman, W. Interlisp Reference Manual. Xerox Palo Alto Res. Ctr., Palo Alto, Calif., 1975.
• 15: Weissman, C. LISP 1.5 Primer, Dickenson, Encino, Calif., 1967.
• 16: Wulf, W.A., London, R.L., and Shaw, M. Abstraction and verification in Alphard: Introduction to language and methodology. Tech. Reports, Inform. Sci. Inst., U. of Southern California, Marina del Rey, Calif., and Carnegie-Mellon U., Pittsburgh, Pa., 1976.
• 17: Wulf, W.A., London, R.L., and Shaw, M. An introduction to the construction and verification of Alphard programs. 1EEE Trans. on Software Eng. SE-2, 4 (Dec. 1976), 253-265.

INDEX TERMS

Keywords:
abstraction and representation, abstraction data types, assertions, control specialization, correctness, generators, invariants, iteration statements, modular decomposition, program specifications, programming languages, programming methodology, proofs of correctness, types, verification