In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. Semantics assigns computational meaning to valid strings in a programming language syntax. It is closely related to, and often crosses over with, the semantics of mathematical proofs. Semantics describes the processes a computer follows when executing a program in that specific language. This can be done by describing the relationship between the input and output of a program, or giving an explanation of how the program will be executed on a certain platform, thereby creating a model of computation.

History

In 1967, Robert W. Floyd published the paper Assigning meanings to programs; his chief aim was "a rigorous standard for proofs about computer programs, including proofs of correctness, equivalence, and termination". Floyd further wrote: 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 published a paper on Hoare logic seeded by Floyd's ideas, now sometimes collectively called axiomatic semantics. In the 1970s, the terms operational semantics and denotational semantics emerged.

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.