Semantics describes the processes a computer follows whenexecuting 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 certainplatform, thereby creating amodel of computation.
In 1967,Robert W. Floyd published the paperAssigning meanings to programs; his chief aim was "a rigorous standard for proofs about computer programs, includingproofs of correctness, equivalence, and termination".[2][3] Floyd further wrote:[2]
A semantic definition of a programming language, in our approach, is founded on asyntactic definition. It must specify which of the phrases in a syntactically correct program representcommands, and whatconditions must be imposed on an interpretation in the neighborhood of each command.
There are many approaches to formal semantics; these belong to three major classes:
Denotational semantics,[6] whereby each phrase in the language is interpreted as adenotation, 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 offunctional languages often translate the language intodomain theory. Denotational semantic descriptions can also serve as compositional translations from a programming language into the denotational metalanguage and used as a basis for designingcompilers.
Operational semantics,[7] whereby the execution of the language is described directly (rather than by translation). Operational semantics loosely corresponds tointerpretation, although again the "implementation language" of the interpreter is generally a mathematical formalism. Operational semantics may define anabstract machine (such as theSECD machine), and give meaning to phrases by describing the transitions they induce on states of the machine. Alternatively, as with the purelambda calculus, operational semantics can be defined via syntactic transformations on phrases of the language itself;
Axiomatic semantics,[8] whereby one gives meaning to phrases by describing theaxioms that apply to them. Axiomatic semantics makes no distinction between a phrase's meaning and the logical formulas that describe it; its meaningis exactly what can be proven about it in some logic. The canonical example of axiomatic semantics isHoare 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.[citation needed]
Some variations of formal semantics include the following:
Action semantics[9] 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;
Attribute grammars[10] define systems that systematically compute "metadata" (calledattributes) for the various cases ofthe 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 incompilers, and to augmentregular orcontext-free grammars withcontext-sensitive conditions;
Categorical (or "functorial") semantics[11] usescategory theory as the core mathematical formalism. 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;[12]
Concurrency semantics[13] is a catch-all term for any formal semantics that describes concurrent computations. Historically important concurrent formalisms have included theactor model andprocess calculi;
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 asimulation 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.
^Schmidt, David A. (1986).Denotational Semantics: A Methodology for Language Development. William C. Brown Publishers.ISBN9780205104505.
^Plotkin, Gordon D. (1981). A structural approach to operational semantics (Report). Technical Report DAIMI FN-19. Computer Science Department,Aarhus University.
^Deransart, Pierre; Jourdan, Martin; Lorho, Bernard (1988)."Attribute Grammars: Definitions, Systems and Bibliography. Lecture Notes in Computer Science 323.Springer-Verlag.ISBN9780387500560.
Hennessy, M. (1990).The semantics of programming languages: an elementary introduction using structural operational semantics. Wiley.ISBN978-0-471-92772-3.
