A case study in specifying the semantics of a programming language

ABSTRACT

On and off over the period of about a year I have worked on a semantic specification for the C programming language My objective was to construct a readable and precise specification of C, aimed at compiler writers, maintainers, and language pundits. This paper is a report on the project.

REFERENCES

• 1: abd75 S. K. Abdali, A lambda calculus model of programming languages: I. simple constructs; II. jumps and procedures, Computer Languages 1, 4 (1975) 287-301,303-320.
• 2: The Vienna Development Method: The Meta-Language, January 1978
• 3: Robert L. Constable , James E. Donahue, A Hierarchical Approach to Formal Semantics With Application to the Definition of PL/ CS, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.1, p.98-114, July 1979 [doi>10.1145/357062.357069]
• 4: cou79 P. Cousot and R. Cousot, Constructive versions of Tarski's fixed point theorems, Pacific J. Math to appear.
• 5: don78 V. Donzeau-Gouge, G. Kahn, and B. Lang, A complete machine-checked definition of a simple programming language using denotational semantics, Rapport de Recherche No 330, IRIA Laboria, Rocquencourt France, (October 1978).
• 6: gor78 M. Gordon, Notes on the descriptive techniques of denotational semantics, University of Edinburgh (February 1978).
• 7: I. Greif , A. Meyer, Specifying programming language semantics: a tutorial and critique of a paper by Hoare and Lauer, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.180-189, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567769]
• 8: Wolfgang Henhapl , Cliff B. Jones, A Formal Definition of Algol 60 as Described in the 1975 Modified Report, The Vienna Development Method: The Meta-Language, p.305-336, January 1978
• 9: C. A. R. Hoare, Some Properties of Predicate Transformers, Journal of the ACM (JACM), v.25 n.3, p.461-480, July 1978 [doi>10.1145/322077.322088]
• 10: joh75 S. C. Johnson, YACC --- Yet another compiler-compiler, Computing Science Technical Report No 32, Bell Laboratories, Murray Hill, New Jersey, (July 1975).
• 11: S. C. Johnson, A portable compiler: theory and practice, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-104, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512771]
• 12: joh79 S. C. Johnson, Lint, a C program checker, in UNIXTime Sharing System:UNIXProgrammers Manual, Volume 24, Bell Laboratories, Murray Hill NJ (January 1979).
• 13: Cliff B. Jones, Denotational Semantics of GOTO: An Exit Formulation and Its Relation to Continuations, The Vienna Development Method: The Meta-Language, p.278-304, January 1978
• 14: B. W. Kernighan , D. M. Ritchie, The C programming language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1978
• 15: luc70 P. Lucas and K. Walk, On the formal description of PL/I, Annual Review in Automatic Programming 6, 3 (1970) 105-182.
• 16: mil72 R. E. Milne, The mathematical semantics of Algol 68, unpublished manuscript, Programming Research Group, Oxford University, (1972).
• 17: Robert Milne , C. Strachey, A Theory of Programming Language Semantics, Halsted Press, New York, NY, 1977
• 18: mor70 F. L. Morris, The next 700 programming language descriptions, unpublished manuscript, (November 1970).
• 19: mos74 P. D. Mosses, The mathematical semantics of Algol 60, Technical Monograph PRG-12, Programming Research Group, Oxford University, (1974).
• 20: mos78 P. D. Mosses, SIS: A compiler-generator system using denotational semantics (Reference Manual), Draft, ref. nr. 78-4-3, Department of Computer Science, University of Aarhus, Denmark, (June 1978).
• 21: rit78 D. M. Ritchie, S. C. Johnson, M. E. Lesk, and B. W. Kernighan, The C programming language, BSTJ 57, 6 part 2 (July-August 1978) 1991-2020.
• 22: rit 79 D. M. Ritchie, A tour through the UNIX C compiler, in UNIXTime Sharing System:UNIXProgrammers Manual, Volume 2B, Bell Laboratories, Murray Hill NJ (January 1979).
• 23: Barry K. Rosen, Applications of high level control flow, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.38-47, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512955]
• 24: scs71 D. S. Scott and C. Strachey, Towards a mathematical semantics for computer languages, Proceedings of the Symposium on Computers and Automata Polytechnic Press, Brooklyn, New York, (April 1971) 19-46.
• 25: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 26: str72 C. Strachey, Varieties of programming language, Proceedings, International Computing Symposium, Cini Foundation, Venice (April 1972) 222-233.
• 27: stw74 C. Strachey and C. Wadsworth, Continuations: a mathematical semantics which can deal with full jumps, Technical Monograph PRG-11, Programming Research Group, Oxford University, ( 1974).
• 28: R. D. Tennent, Mathematical semantics of SNOBOL4, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.95-107, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512936]
• 29: R. D. Tennent, The denotational semantics of programming languages, Communications of the ACM, v.19 n.8, p.437-453, Aug. 1976 [doi>10.1145/360303.360308]
• 30: ten77 R. D. Tennent, A denotational definition of the programming language Pascal, Technical Report 77-47, Department of Computing and Information Science, Queen's University, Kingston, Canada, (July 1977).