Abstract
An axiomatic treatment of ALGOL 68 routines (procedures and functions) is presented. An approach to axiomatically defining the semantics of an expression-oriented language is first introduced. Using this, rules of inference for routines are given. The rules contain no aliasing restrictions, allow parameters of arbitrary modes including routines, treat full static scoping of identifiers, and allow side-effects to global variables. Attendant issues in language design and verification are also discussed.
This work was supported in part by an IBM Doctoral Fellowship at the University of California at Los Angeles, and in part by a Weizmann Post-Doctoral Fellowship at the Weizmann Institute of Science.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Cartwright, R., D. Oppen. "Unrestricted Procedure Calls in Hoare's Logic," Proceedings of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tuscon, Arizona, January 1978.
Clarke, E. "Pathological Interaction of Programming Language Features," Computer Science Department, Duke University, Report CS-1976-15, September 1976.
Clarke, E. "Programming Language Constructs for which it is Impossible to Obtain Good Hoare-like Axiom Systems," Proceedings of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, January 1977.
Cook, S.A. "Soundness and Completeness of an Axiom System for Program Verification," Computer Science Department, University of Toronto, Report 95, June 1976.
Department of Defense. Blue Programming Language Specification, February 1978.
Department of Defense. Green Programming Language Specification, February 1978.
Department of Defense. Red Programming Language Specification, February 1978.
Department of Defense. Yellow Programming Language Specification, February 1978.
Floyd, R.W. "Assigning Meanings to Programs," Proceedings of the Symposium of Applied Mathematics, 19, in J.T. Schwartz, Editor, Mathematical Aspects of Computer Science, pp. 19–32, American Mathematical Society, Providence, Rhode Island, 1967.
Fokkinga, M. "Axiomatization of Declarations and the Formal Treatment of an Escape Construct," IFIP Technical Committee 2 Meeting, Toronto Canada, August 1977.
Gorelick, S. "A Complete Axiomatic System for Proving Assertions about Recursive and Non-Recursive Programs," Computer Science Department, University of Toronto, Report 75, January 1975.
Guttag, J., J. Horning, R. London. "A Proof Rule for EUCLID Procedures," in E. Neuhold, Editor, Formal Description of Programming Concepts, North Holland Publishing Company, 1978.
Hoare, C.A.R. "An Axiomatic Basis for Computer Programming," Communications of the ACM, 12:10, October 1969.
Hoare, C.A.R. "Procedures and Parameters: An Axiomatic Approach," Symposium on Semantics of Algorithmic Languages, E. Engeler, Editor, Springer Verlag, pp. 102–116, 1971.
Lampson, B., et al. "Report on the Programming Language EUCLID," SIGPLAN Notices, 12:2, 1977.
London, R., private communication, August 1978.
Naur, P., Editor. "Revised Report on the Algorithmic Language ALGOL 60," Communications of the ACM, 6:3, March 1963.
Owicki, S. Axiomatic Proof Techniques for Parallel Programs, Ph.D. Dissertation, Cornell University, Ithaca, New York, 1975.
Schwartz, R. "An Axiomatic Semantic Definition of ALGOL 68," Computer Science Department, University of California at Los Angeles, UCLA-34-P214-75, August 1978 (Ph.D. Dissertation).
Schwartz, R. "An Axiomatic Treatment of Asynchronous Parallel Processes in ALGOL 68," submitted for publication, January 1979.
Schwartz, R. "On Axiomatizability as a Language Design Tool," January 1979.
Schwartz, R., D. Berry. "A Semantic View of ALGOL 68," Journal of Computer Languages, Vol. 4, No. 1, 1979.
Tanenbaum, A. "A Tutorial on ALGOL 68," ACM Computing Surveys, Vol. 8, No. 2, June 1976.
van Wijngaarden, A., Editor. "Report on the Algorithmic Language ALGOL 68," Numerische Mathematik, 14, pp. 79–218, 1969.
van Wijngaarden, A., et al., Editor. "Revised Report on the Algorithmic Language ALGOL 68," Acta Informatica, 5, 1975.
Wirth, N. "The Programming Language PASCAL," Acta Informatica, 1, pp. 35–63, 1971.
Wulf, W., R.L. London, M. Shaw. "Abstraction and Verification in ALPHARD: Introduction to Language and Methodology," Information Sciences Institute Technical Report ISI/RR-76-46, Marina del Rey, California, June 1976.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1979 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schwartz, R.L. (1979). An axiomatic treatment of ALGOL 68 routines. In: Maurer, H.A. (eds) Automata, Languages and Programming. ICALP 1979. Lecture Notes in Computer Science, vol 71. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-09510-1_43
Download citation
DOI: https://doi.org/10.1007/3-540-09510-1_43
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-09510-1
Online ISBN: 978-3-540-35168-9
eBook Packages: Springer Book Archive