In
programming language theory, semantics is the rigorous mathematical study of the meaning of
programming language
A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language.
The description of a programming ...
s. Semantics assigns
computational meaning to valid
strings in a
programming language syntax
In computer science, the syntax of a computer language is the rules that defines the combinations of symbols that are considered to be correctly structured statements or expressions in that language. This applies both to programming languages ...
.
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
Platform may refer to:
Technology
* Computing platform, a framework on which applications may be run
* Platform game, a genre of video games
* Car platform, a set of components shared by several vehicle models
* Weapons platform, a system or ...
, 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 how ...
.
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, and what conditions must be imposed on an interpretation in the neighborhood of each command.
In 1969,
Tony Hoare
Sir Charles Antony Richard Hoare (Tony Hoare or C. A. R. Hoare) (born 11 January 1934) is a British computer scientist who has made foundational contributions to programming languages, algorithms, operating systems, formal verification, and ...
publishes a paper on
Hoare logic seeded by Floyd's ideas, now sometimes collectively called ''
axiomatic semantics''.
In the 1970s, the terms ''
operational semantics
Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execut ...
'' 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 premise ...
,
set theory
Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly conce ...
,
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 (includi ...
such as
programming language design,
type theory
In mathematics, logic, and computer science, a type theory is the 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 theory as a fou ...
,
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 tha ...
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
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal metho ...
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
In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that m ...
often translate the language into
domain theory
Domain theory is a branch of mathematics that studies special kinds of partially ordered sets (posets) commonly called domains. Consequently, domain theory can be considered as a branch of order theory. The field has major applications in computer ...
. 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 tha ...
s.
*
Operational semantics
Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execut ...
, 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
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 pr ...
(such as the
SECD machine The SECD machine is a highly influential (''see: '') virtual machine and abstract machine intended as a target for functional programming language compilers. The letters stand for Stack, Environment, Control, Dump—the internal registers of the mac ...
), 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.
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 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 mathematics.
Elementary ...
ic laws for describing and reasoning about program semantics
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 ...
in a formal manner. It also supports denotational semantics and operational semantics
Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execut ...
;
* Attribute grammar An attribute grammar is a formal way to supplement a formal grammar with semantic information processing. Semantic information is stored in attributes associated with terminal and nonterminal symbols of the grammar. The values of attributes are resu ...
s 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 tha ...
s, and to augment regular or context-free grammars
In formal language theory, a context-free grammar (CFG) is a formal grammar whose production rules are of the form
:A\ \to\ \alpha
with A a ''single'' nonterminal symbol, and \alpha a string of terminals and/or nonterminals (\alpha can be empt ...
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 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
In computer science, the process calculi (or process algebras) are a diverse family of related approaches for formally modelling concurrent systems. Process calculi provide a tool for the high-level description of interactions, communications, and ...
;
* Game semantics
Game semantics (german: dialogische Logik, translated as ''dialogical logic'') is an approach to Formal semantics (logic), formal semantics that grounds the concepts of truth or Validity (logic), validity on game theory, game-theoretic concepts, su ...
uses a metaphor inspired by game theory;
* Predicate transformer semantics
Predicate transformer semantics were introduced by Edsger Dijkstra in his seminal paper " Guarded commands, nondeterminacy and formal derivation of programs". They define the semantics of an imperative programming paradigm by assigning to each ''st ...
, developed by Edsger W. Dijkstra, describes the meaning of a program fragment as the function transforming a postcondition In computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions wit ...
to the precondition
In computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification.
If a precondition is violated, the effect of the s ...
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 s ...
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
Computational semantics is the study of how to automate the process of constructing and reasoning with meaning representations of natural language expressions. It consequently plays an important role in natural-language processing and computatio ...
* Formal semantics (logic)
In logic, the semantics of logic or formal semantics is the study of the semantics, or interpretations, of formal and (idealizations of) natural languages usually trying to capture the pre-theoretic notion of entailment.
Overview
The truth con ...
* Formal semantics (linguistics)
Formal semantics is the study of grammatical meaning in natural languages using formal tools from logic and theoretical computer science. It is an interdisciplinary field, sometimes regarded as a subfield of both linguistics and philosophy of lang ...
* 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 exi ...
* Ontology (information science)
* Semantic equivalence {{about, semantic equivalence of metadata, the concept in mathematical logic, Logical equivalence
In computer metadata, semantic equivalence is a declaration that two data elements from different vocabularies contain data that has similar meaning. ...
* Semantic technology
The ultimate goal of semantic technology is to help machines understand data. To enable the encoding of semantics with the data, well-known technologies are RDF (Resource Description Framework) and OWL (Web Ontology Language). These technologies ...
References
Further reading
; Textbooks
*
*
*
*
*
*
*
*
*
* (Working draft)
*
*
*
; Lecture notes
*
External links
* Semantics.
{{DEFAULTSORT:Semantics Of Programming Languages
Formal methods
Logic in computer science