This article includes a list of general references, but it lacks sufficient corresponding inline citations. Please help to improve this article by introducing more precise citations. (August 2020) (Learn how and when to remove this template message)

In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages.[1] Semantics assigns computational meaning to valid strings in a programming language syntax.

Semantics describes the processes a computer follows when executing a program in that specific language. This can be shown by describing the relationship between the input and output of a program, or an explanation of how the program will be executed on a certain platform, hence creating a model of computation.

History

In 1967, Robert W. Floyd publishes the paper Assigning meanings to programs; his chief aim is "a rigorous standard for proofs about computer programs, including proofs of correctness, equivalence, and termination".[2][3] Floyd further writes:[2]

A semantic definition of a programming language, in our approach, is founded on a syntactic definition. It must specify which of the phrases in a syntactically correct program represent commands, and what conditions must be imposed on an interpretation in the neighborhood of each command.

In 1969, Tony Hoare publishes a paper on Hoare logic seeded by Floyd's ideas, now sometimes collectively called axiomatic semantics.[4][5]

In the 1970s, the terms operational semantics and denotational semantics emerged.[5]

Overview

The field of formal semantics encompasses all of the following:

It has close links with other areas of computer science such as programming language design, type theory, compilers and interpreters, program verification and model checking.

Approaches

There are many approaches to formal semantics; these belong to three major classes:

Apart from the choice between denotational, operational, or axiomatic approaches, most variations in formal semantic systems arise from the choice of supporting mathematical formalism.

Variations

Some variations of formal semantics include the following:

Describing relationships

For a variety of reasons, one might wish to describe the relationships between different formal semantics. For example:

It is also possible to relate multiple semantics through abstractions via the theory of abstract interpretation.

See also

References

  1. ^ Joseph A. Goguen (1975). "Semantics of computation". Category Theory Applied to Computation and Control. Lecture Notes in Computer Science. Vol. 25. Springer. pp. 151–163. doi:10.1007/3-540-07142-3_75. ISBN 978-3-540-07142-6.
  2. ^ a b Floyd, Robert W. (1967). "Assigning Meanings to Programs" (PDF). In Schwartz, J.T. (ed.). Mathematical Aspects of Computer Science. Proceedings of Symposium on Applied Mathematics. Vol. 19. American Mathematical Society. pp. 19–32. ISBN 0821867288.
  3. ^ Donald E. Knuth. "Memorial Resolution: Robert W. Floyd (1936–2001)" (PDF). Stanford University Faculty Memorials. Stanford Historical Society.
  4. ^ Hoare, C. A. R. (October 1969). "An axiomatic basis for computer programming". Communications of the ACM. 12 (10): 576–580. doi:10.1145/363235.363259. S2CID 207726175.
  5. ^ a b Winskel, Glynn (1993). The formal semantics of programming languages : an introduction. Cambridge, Mass.: MIT Press. p. xv. ISBN 978-0-262-23169-5.
  6. ^ David A. Schmidt (1986). Denotational Semantics: A Methodology for Language Development. William C. Brown Publishers. ISBN 9780205104505.
  7. ^ Gordon D. Plotkin (1981). "A structural approach to operational semantics". Technical Report DAIMI FN-19. Computer Science Department, Aarhus University. ((cite journal)): Cite journal requires |journal= (help)
  8. ^ a b Joseph A. Goguen; James W. Thatcher; Eric G. Wagner; Jesse B. Wright (1977). "Initial algebra semantics and continuous algebras". Journal of the ACM. 24 (1): 68–95. doi:10.1145/321992.321997. S2CID 11060837.
  9. ^ Peter D. Mosses (1996). "Theory and practice of action semantics". BRICS Report RS9653. Aarhus University. ((cite journal)): Cite journal requires |journal= (help)
  10. ^ Pierre Deransart; Martin Jourdan; Bernard Lorho (1988). "Attribute Grammars: Definitions, Systems and Bibliography. Lecture Notes in Computer Science 323. Springer-Verlag. ISBN 9780387500560.
  11. ^ F. William Lawvere (1963). "Functorial semantics of algebraic theories". Proceedings of the National Academy of Sciences of the United States of America. 50 (5): 869–872. Bibcode:1963PNAS...50..869L. doi:10.1073/pnas.50.5.869. PMC 221940. PMID 16591125.
  12. ^ Andrzej Tarlecki; Rod M. Burstall; Joseph A. Goguen (1991). "Some fundamental algebraic tools for the semantics of computation: Part 3. Indexed categories". Theoretical Computer Science. 91 (2): 239–264. doi:10.1016/0304-3975(91)90085-G.
  13. ^ Mark Batty; Kayvan Memarian; Kyndylan Nienhuis; Jean Pichon-Pharabod; Peter Sewell (2015). "The problem of programming language concurrency semantics". Proceedings of the European Symposium on Programming Languages and Systems. Springer. pp. 283–307. doi:10.1007/978-3-662-46669-8_12.
  14. ^ Samson Abramsky (2009). "Semantics of interaction: An introduction to game semantics". In Andrew M. Pitts; P. Dybjer (eds.). Semantics and Logics of Computation. Cambridge University Press. pp. 1–32. doi:10.1017/CBO9780511526619.002. ISBN 9780521580571.
  15. ^ Edsger W. Dijkstra (1975). "Guarded commands, nondeterminacy and formal derivation of programs". Communications of the ACM. 18 (8): 453–457. doi:10.1145/360933.360975. S2CID 1679242.

Further reading

Textbooks
Lecture notes

External links[edit]