A Case Study in Specifying the Denotational Semantics of C
C is a well known and very popular general purpose programming language which represents, together with its descendants, a strong and indisputable status quo in the current software industry. Its semantics is informally defined in the ISO/IEC 9899:1990 standard  using natural language. This causes a number of ambiguities and problems of interpretation, clearly manifested in numerous discussions taking place in the newsgroup comp. std. c. It is worthwhile noticing that members of the standardization committee and other distinguished researchers participating in the discussions often give contradictory answers when asked about the intended semantics of surprisingly small programs, and that their answers are usually based on different possible interpretations of the standard. With all this in mind, the necessity for a formal description of the semantics of C becomes apparent. Such a description would serve as a precise standard for compiler implementation and would provide a basis for reasoning about properties of C programs.
KeywordsTyping Semantic Static Semantic Typing Rule Type Environment Denotational Semantic
Unable to display preview. Download preview PDF.
- American National Standards Institute, New York, NY. ANSI/ISO 9899–1990, American National Standard for Programming Languages: C, 1990. Revision and redesignation of ANSI X3.159-1989.Google Scholar
- R. Sethi. A case study in specifying the semantics of a programming language. In Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages, pages 117–130, January 1980.Google Scholar
- Y. Gurevich and J. K. Huggins. The semantics of the C programming language. In E. Börger et al., editors, Selected Papers from CSL′92 (Computer Science Logic), volume 702 of Lecture Notes in Computer Science, pages 274–308. Springer Verlag, New York, NY, 1993.Google Scholar
- J. Cook and S. Subramanian. A formal semantics for C in Nqthm. Technical Report 517D, Trusled Information Systems, October 1994.Google Scholar
- J. Cook, E. Cohen, and T. Redmond. A ibrmal denotational semantics for C. Technical Report 409D, Trusted Information Systems, September 1994.Google Scholar
- M. Norrish. An abstract dynamic semantics for C. Technical Report TR-421, University of Cambridge. Computer Laboratory, May 1997.Google Scholar
- N. S. Papaspyrou. A Formal Semantics for the C Programming Language. PhD thesis, National Technical University of Athens, Software Engineering Laboratory, February 1998.Google Scholar
- P. D. Mosses. Denotationai semantics. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 11, pages 577–631. Elsevier Science Publishers B.V., 1990.Google Scholar
- E. Moggi. An abstract view of programming languages. Technical Report ECS-LFCS-90-113, University of Edinburgh, Laboratory for Foundations of Computer Science, 1990.Google Scholar
- P. Wadler. The essence of functional programming. Ir. Proceedings of the 19th Annual Symposium on Principles of Programming Languages (POPL ′92), January 1992.Google Scholar
- S. Liang, P. Hudak, and M. Jones. Monad transformers and modular interpreters. In Conference Record of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ′95). San Francisco, CA, January 1995.Google Scholar