Abstraction and Verification in Alphard: Design and Verification of a Tree Handler

  • Mary Shaw

Abstract

The design of the Alphard programming language has been strongly influenced by ideas from the areas of programming methodology and formal program verification. The interaction of these ideas and their influence on Alphard are described by developing a nontrivial example, a program for manipulating the parse tree of an arithmetic expression.

Keywords

Assure Ather Mellon 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Dahl72]
    O.-J. Dahl and C. A. R. Hoare, “Hierarchical Program Structures”, in Structured Programming ( Dahl, Dijkstra, and Hoare ), Academic Press, 1972 (pp. 175–220 ).Google Scholar
  2. [Dijkstra72]
    Edsger W. Dijkstra, “Notes on Structured Programming”, in Structured Programming ( Dahl, Dijkstra, and Hoare ), Academic Press, 1972 (pp. 1–82 ).Google Scholar
  3. [Hoare72]
    C. A. R. Hoare, “Proof of Correctness of Data Representations”, Acta Informatica, 1, 4, 1972 (pp. 271–281 ).CrossRefGoogle Scholar
  4. [Johnsson75]
    Richard K. Johnsson, “An Approach to Global Register Allocaton”, Carnegie-Mellon University Technical Report, December 1975.Google Scholar
  5. [Knuth73]
    Donald E. Knuth, Fundamental Algorithms, Second Edition, Addison-Wesley, 1973.Google Scholar
  6. [Liskov74]
    Barbara Liskov and Stephen Zilles, “Programming with Abstract Data Types”, SIGPLAN Notices, 9,4, April 1974 (pp. 50–59 ).Google Scholar
  7. [Nakata67]
    Ikuo Nakata, “A Note on Compiling Algorithms for Arithmetic Expressions”, Communications of the ACM, 10, 8, August 1967.CrossRefGoogle Scholar
  8. [Parnas72]
    David L. Parnas, “On the Criteria to be Used in Decomposing Systems into Modules”, Communications of the ACM, 15, 12, December 1972 (pp. 1053–1058 ).CrossRefGoogle Scholar
  9. [Shaw76]
    Mary Shaw, William Wulf, and Ralph L London, “Abstraction and Verification in Alphard: Iteration and Generators”, Carnegie-Mellon University Technical Report and USC Information Sciences Institute Research Report, 1976.Google Scholar
  10. [Wirth71]
    Niklaus Wirth, “Program Development by Stepwise Refinement”, Communications of the ACM, 14, 4, April 1971 (pp. 221–227 ).MATHCrossRefGoogle Scholar
  11. [Wulf76]
    William Wulf, Ralph L. London, and Mary Shaw, “Abstraction and Verification in Alphard: Introduction to Language and Methodology”, Carnegie-Mellon University Technical Report and USC Information Sciences Institute Research Report, 1976.Google Scholar

Copyright information

© Springer-Verlag New York Inc. 1981

Authors and Affiliations

  • Mary Shaw
    • 1
  1. 1.Carnegie-Mellon UniversityUSA

Personalised recommendations