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.
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
In computer science, and more specifically in computability theory and computational complexity theory, a model of computation is a model which describes how an output of a mathematical function is computed given an input. A model describes h ...
.
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".
Floyd further writes:
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
Command may refer to:
Computing
* Command (computing), a statement in a computer language
* COMMAND.COM, the default operating system shell and command-line interpreter for DOS
* Command key, a modifier key on Apple Macintosh computer keyboards
* ...
, 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''.
In the 1970s, the terms ''
operational semantics'' and ''
denotational semantics'' emerged.
Overview
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
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premis ...
,
set theory,
model theory,
category theory, etc.
It has close links with other areas of
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includin ...
such as
programming language design,
type theory
In mathematics, logic, and computer science, a type theory is the formal system, formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theor ...
,
compiler
In computing, a compiler is a computer program that translates computer code written in one programming language (the ''source'' language) into another language (the ''target'' language). The name "compiler" is primarily used for programs that ...
s and
interpreters
Interpreting is a translational activity in which one produces a first and final target-language output on the basis of a one-time exposure to an expression in a source language.
The most common two modes of interpreting are simultaneous interp ...
,
program verification and
model checking.
Approaches
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
compiler
In computing, a compiler is a computer program that translates computer code written in one programming language (the ''source'' language) into another language (the ''target'' language). The name "compiler" is primarily used for programs that ...
s.
*
Operational semantics, whereby the execution of the language is described directly (rather than by translation). Operational semantics loosely corresponds to
interpretation
Interpretation may refer to:
Culture
* Aesthetic interpretation, an explanation of the meaning of a work of art
* Allegorical interpretation, an approach that assumes a text should not be interpreted literally
* Dramatic Interpretation, an event ...
, although again the "implementation language" of the interpreter is generally a mathematical formalism. Operational semantics may define an
abstract machine
An abstract machine is a computer science theoretical model that allows for a detailed and precise analysis of how a computer system functions. It is analogous to a mathematical function in that it receives inputs and produces outputs based on p ...
(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 ''
axiom
An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy o ...
s'' 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.
Variations
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 ]algebra
Algebra () is one of the areas of mathematics, broad areas of mathematics. Roughly speaking, algebra is the study of mathematical symbols and the rules for manipulating these symbols in formulas; it is a unifying thread of almost all of mathem ...
ic laws for describing and reasoning about program semantics in a formal
Formal, formality, informal or informality imply the complying with, or not complying with, some set of requirements (forms, in Ancient Greek). They may refer to:
Dress code and events
* Formal wear, attire for formal events
* Semi-formal attire ...
manner. It also supports denotational semantics and operational semantics;
* 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 compiler
In computing, a compiler is a computer program that translates computer code written in one programming language (the ''source'' language) into another language (the ''target'' language). The name "compiler" is primarily used for programs that ...
s, and to augment regular
The term regular can mean normal or in accordance with rules. It may refer to:
People
* Moses Regular (born 1971), America football player
Arts, entertainment, and media Music
* "Regular" (Badfinger song)
* Regular tunings of stringed instrum ...
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;
* Concurrency semantics
In computer science, concurrency semantics is a way to give meaning to concurrent systems in a mathematically rigorous way. Concurrency semantics is often based on mathematical theories of concurrency such as various process calculi, the actor mo ...
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
Edsger Wybe Dijkstra ( ; ; 11 May 1930 – 6 August 2002) was a Dutch computer scientist, programmer, software engineer, systems scientist, and science essayist. He received the 1972 Turing Award for fundamental contributions to developing progra ...
, describes the meaning of a program fragment as the function transforming a postcondition to the precondition needed to establish it.
Describing relationships
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
A simulation is the imitation of the operation of a real-world process or system over time. Simulations require the use of models; the model represents the key characteristics or behaviors of the selected system or process, whereas the ...
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.
See also
* Computational semantics
* Formal semantics (logic)
* Formal semantics (linguistics)
* Ontology
In metaphysics, ontology is the philosophical study of being, as well as related concepts such as existence, becoming, and reality.
Ontology addresses questions like how entities are grouped into categories and which of these entities ...
* Ontology (information science)
In computer science and information science, an ontology encompasses a representation, formal naming, and definition of the categories, properties, and relations between the concepts, data, and entities that substantiate one, many, or all domai ...
* Semantic equivalence
* Semantic technology
References
Further reading
; Textbooks
*
*
*
*
*
*
*
*
*
* (Working draft)
*
*
*
; Lecture notes
*
External links
* Semantics.
{{DEFAULTSORT:Semantics Of Programming Languages
Formal methods
Logic in computer science