On the essence of Oberon

  • David A. Naumann
Session Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 782)


Reynolds described the “essence of Algol” as the simple imperative language combined with the typed lambda calculus. We provide a similar description of Wirth's language Oberon as the simple imperative language combined with procedure types and record extension. Whereas the semantics of Algol has been given in terms of a (domain theoretic) model using an explicit representation of storage, our semantics uses predicate transformers; this is possible thanks to recent advances in the theory of predicate transformers. Predicate transformer semantics connects one of the most successful methods of rigorous program development with one of the most successful pragmatically-designed programming languages.


Procedure Variable Specification Constant Type Extension State Predicate Predicate Transformer 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    K.R. Apt. Ten years of hoare's logic, a survey, part I. ACM Transactions on Programming Languages and Systems, 3, 1981.Google Scholar
  2. 2.
    R. J. R. Back. Correctness preserving program refinements: Proof theory and applications. Technical Report Tract 131, CWI, 1980.Google Scholar
  3. 3.
    A. Bijlsma. Calculating with procedure calls. Information Processing Letters, 46:211–217, 1993.Google Scholar
  4. 4.
    Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.Google Scholar
  5. 5.
    Paul Gardiner and Carroll Morgan. Data refinement of predicate transformers. Theoretical Computer Science, 87:143–162, 1991.Google Scholar
  6. 6.
    C.A.R. Hoare, J. He, and A. Sampaio. Normal form approach to compiler design. to appear in Acta Informatica, 1993.Google Scholar
  7. 7.
    C.A.R. Hoare and Jifeng He. Data refinement in a categorical setting. Technical Monograph PRG-PRG-90, November 1990.Google Scholar
  8. 8.
    Anne Kaldewaij. Programming: the Derivation of Algorithms. Prentice-Hall, 1990.Google Scholar
  9. 9.
    Clare E. Martin. Preordered categories and predicate transformers. Dissertation, Oxford University, 1991.Google Scholar
  10. 10.
    Carroll Morgan. Procedures, parameters, and abstraction: Separate concerns. Science of Computer Programming, 11(1), 1988.Google Scholar
  11. 11.
    Carroll Morgan. Programming from Specifications. Prentice Hall, 1990.Google Scholar
  12. 12.
    David A. Naumann. Predicate transformers and higher order programs. Submitted to Theoretical Computer Science, 1992.Google Scholar
  13. 13.
    David A. Naumann. Two-categories and program structure: Data types, refinement calculi, and predicate transformers. Dissertation, University of Texas at Austin, 1992.Google Scholar
  14. 14.
    David A. Naumann. Data refinement, call by value, and higher types. Submitted to Science of Computer Programming, 1993.Google Scholar
  15. 15.
    P. W. O'Hearn and R. D. Tennant. Relational parametricity and local variables (preliminary report). In Proceedings, Twentieth POPL, pages 171–184, 1993.Google Scholar
  16. 16.
    Martin Reiser and Niklaus Wirth. Programming in Oberon. Addison-Wesley, 1992.Google Scholar
  17. 17.
    John C. Reynolds. The Craft of Programming. Prentice-Hall, 1981.Google Scholar
  18. 18.
    John C. Reynolds. The essence of Algol. In J. W. de Bakker and J. C. van Vliet, editors, Algorithmic Languages. North-Holland, 1981.Google Scholar
  19. 19.
    R. D. Tennant. Semantical analysis of specification logic. Information and Computation, 85, 1990.Google Scholar
  20. 20.
    R.D. Tennant. Semantics of Programming Languages. Prentice Hall, 1991.Google Scholar
  21. 21.
    Stephen Weeks and Matthias Felleisen. On the orthogonality of assignments and procedures in Algol. In Proceedings, Twentieth POPL, 1993.Google Scholar
  22. 22.
    N. Wirth. The programming language Oberon. Software — Practice and Experience, 18(7), 1988.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • David A. Naumann
    • 1
  1. 1.Southwestern UniversityGeorgetownUSA

Personalised recommendations