Formal Semantics of Programming Languages

Learn about Formal semantics of programming languages topic at defaultLogic. defaultLogic provides comprehensive technology and business learning resources.

## Overview

## Approaches

## Variations

## Describing relationships

## History

## See also

## References

## Further reading

## External links

This article uses material from the Wikipedia page available here. It is released under the Creative Commons Attribution-Share-Alike License 3.0.

This article includes a list of general references, but it remains largely unverified because it lacks sufficient corresponding inline citations. (August 2020) |

In programming language theory, **semantics** is the field concerned with the rigorous mathematical study of the meaning of programming languages.^{[1]}
It does so by evaluating the meaning of syntactically valid strings defined by a specific programming language, showing the computation involved. In such a case that the evaluation would be of syntactically invalid strings, the result would be non-computation. 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.

The field of formal semantics encompasses all of the following:

- The definition of semantic models
- The relations between different semantic models
- The relations between different approaches to meaning
- The relation between computation and the underlying mathematical structures from fields such as logic, set theory, model theory, category theory, etc.

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.

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

**Denotational semantics**, whereby each phrase in the language is interpreted as a*denotation*, i.e. a conceptual meaning that can be thought of abstractly. Such denotations are often mathematical objects inhabiting a mathematical space, but it is not a requirement that they should be so. As a practical necessity, denotations are described using some form of mathematical notation, which can in turn be formalized as a denotational metalanguage. For example, denotational semantics of functional languages often translate the language into domain theory. Denotational semantic descriptions can also serve as compositional translations from a programming language into the denotational metalanguage and used as a basis for designing compilers.**Operational semantics**, whereby the execution of the language is described directly (rather than by translation). Operational semantics loosely corresponds to interpretation, although again the "implementation language" of the interpreter is generally a mathematical formalism. Operational semantics may define an abstract machine (such as the SECD machine), and give meaning to phrases by describing the transitions they induce on states of the machine. Alternatively, as with the pure lambda calculus, operational semantics can be defined via syntactic transformations on phrases of the language itself;**Axiomatic semantics**, whereby one gives meaning to phrases by describing the*axioms*that apply to them. Axiomatic semantics makes no distinction between a phrase's meaning and the logical formulas that describe it; its meaning*is*exactly what can be proven about it in some logic. The canonical example of axiomatic semantics is Hoare logic.

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

Some variations of formal semantics include the following:

**Action semantics**is an approach that tries to modularize denotational semantics, splitting the formalization process in two layers (macro and microsemantics) and predefining three semantic entities (actions, data and yielders) to simplify the specification;**Algebraic semantics**is a form of axiomatic semantics based on algebraic laws for describing and reasoning about program semantics in a formal manner;**Attribute grammars**define systems that systematically compute "metadata" (called*attributes*) for the various cases of the language's syntax. Attribute grammars can be understood as a denotational semantics where the target language is simply the original language enriched with attribute annotations. Aside from formal semantics, attribute grammars have also been used for code generation in compilers, and to augment regular or context-free grammars with context-sensitive conditions;**Categorical (or "functorial") semantics**uses category theory as the core mathematical formalism. A categorical semantics is usually proven to correspond to some axiomatic semantics that gives a syntactic presentation of the categorical structures. Also, denotational semantics are often instances of a general categorical semantics,^{[2]}**Concurrency semantics**is a catch-all term for any formal semantics that describes concurrent computations. Historically important concurrent formalisms have included the actor model and process calculi;**Game semantics**uses a metaphor inspired by game theory.**Predicate transformer semantics**, developed by Edsger W. Dijkstra, describes the meaning of a program fragment as the function transforming a postcondition to the precondition needed to establish it.

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

- To prove that a particular operational semantics for a language satisfies the logical formulas of an axiomatic semantics for that language. Such a proof demonstrates that it is "sound" to reason about a particular (operational)
*interpretation strategy*using a particular (axiomatic)*proof system*. - To prove that operational semantics over a high-level machine is related by a simulation with the semantics over a low-level machine, whereby the low-level abstract machine contains more primitive operations than the high-level abstract machine definition of a given language. Such a proof demonstrates that the low-level machine "faithfully implements" the high-level machine.

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

Robert W. Floyd is credited with founding the field of programming language semantics in Floyd (1967).^{[3]}

- Computational semantics
- Formal semantics (logic)
- Formal semantics (linguistics)
- Ontology
- Ontology (information science)
- Semantic equivalence
- Semantic technology

**^**Joseph Goguen "Semantics of Computation" Conference on Category Theory Applied to Computation and Control, San Francisco, CA, 1974 pp 151-163**^**Andrzej Tarlecki, Rod Burstall, Joseph Goguen Some Fundamental Algebraic Tools for the Semantics of Computation Theoretical Computer Science 91(2) pp 239-264**^**Knuth, Donald E. "Memorial Resolution: Robert W. Floyd (1936-2001)" (PDF).*Stanford University Faculty Memorials*. Stanford Historical Society.

- Textbooks

- 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.**19**. American Mathematical Society. pp. 19-32. ISBN 0821867288. - Hennessy, M. (1990).
*The semantics of programming languages: an elementary introduction using structural operational semantics*. Wiley. ISBN 978-0-471-92772-3. - Tennent, Robert D. (1991).
*Semantics of Programming Languages*. Prentice Hall. ISBN 978-0-13-805599-8. - Gunter, Carl (1992).
*Semantics of Programming Languages*. MIT Press. ISBN 0-262-07143-6. - Nielson, H. R.; Nielson, Flemming (1992).
*Semantics With Applications: A Formal Introduction*(PDF). Wiley. ISBN 978-0-471-92980-2. - Winskel, Glynn (1993).
*The Formal Semantics of Programming Languages: An Introduction*. MIT Press. ISBN 0-262-73103-7. - Mitchell, John C. (1995).
*Foundations for Programming Languages*(Postscript). - Slonneger, Kenneth; Kurtz, Barry L. (1995).
*Formal Syntax and Semantics of Programming Languages*. Addison-Wesley. ISBN 0-201-65697-3. - Reynolds, John C. (1998).
*Theories of Programming Languages*. Cambridge University Press. ISBN 0-521-59414-6. - Harper, Robert (2006).
*Practical Foundations for Programming Languages*(PDF). Archived from the original (PDF) on 2007-06-27. (Working draft) - Nielson, H. R.; Nielson, Flemming (2007).
*Semantics with Applications: An Appetizer*. Springer. ISBN 978-1-84628-692-6. - Stump, Aaron (2014).
*Programming Language Foundations*. Wiley. ISBN 978-1-118-00747-1. - Krishnamurthi, Shriram (2012). "Programming Languages: Application and Interpretation" (2nd ed.).

- Lecture notes

- Winskel, Glynn. "Denotational Semantics" (PDF). University of Cambridge.

- Aaby, Anthony (2004).
*Introduction to Programming Languages*. Archived from the original on 2015-06-19.CS1 maint: bot: original URL status unknown (link) Semantics.

This article uses material from the Wikipedia page available here. It is released under the Creative Commons Attribution-Share-Alike License 3.0.

Popular Products

Music Scenes

Popular Artists