In
computer science
Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...
, algebraic semantics is a formal approach to
programming language theory
Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is clos ...
that uses
algebraic methods for defining, specifying, and
reasoning
Reason is the capacity of consciously applying logic by drawing valid conclusions from new or existing information, with the aim of seeking the truth. It is associated with such characteristically human activities as philosophy, religion, scien ...
about the behavior of
programs. It is a form of
axiomatic semantics
Axiomatic semantics is an approach based on mathematical logic for proving the correctness of computer programs. It is closely related to Hoare logic.
Axiomatic semantics define the meaning of a command in a program by describing its effect on ...
that provides a
mathematical framework for analyzing programs through the use of
algebraic structures
In mathematics, an algebraic structure or algebraic system consists of a nonempty set ''A'' (called the underlying set, carrier set or domain), a collection of operations on ''A'' (typically binary operations such as addition and multiplicatio ...
and
equational logic.
[ ][ ]
Algebraic semantics represents programs and data types as
algebras—mathematical structures consisting of sets equipped with operations that satisfy certain equational laws. This approach enables rigorous
formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics.
Formal ver ...
of software by treating program properties as algebraic properties that can be proven through
mathematical reasoning. A key advantage of algebraic semantics is its ability to separate the specification of what a program does from how it is implemented, supporting
abstraction
Abstraction is a process where general rules and concepts are derived from the use and classifying of specific examples, literal (reality, real or Abstract and concrete, concrete) signifiers, first principles, or other methods.
"An abstraction" ...
and
modularity in software design.
Syntax
The
syntax
In linguistics, syntax ( ) is the study of how words and morphemes combine to form larger units such as phrases and sentences. Central concerns of syntax include word order, grammatical relations, hierarchical sentence structure (constituenc ...
of an
algebraic specification is formulated in two steps: (1) defining a formal signature of data types and operation symbols, and (2) interpreting the signature through sets and functions.
Definition of a signature
The
signature
A signature (; from , "to sign") is a depiction of someone's name, nickname, or even a simple "X" or other mark that a person writes on documents as a proof of identity and intent. Signatures are often, but not always, Handwriting, handwritt ...
of an algebraic specification defines its formal syntax. The word "signature" is used like the concept of "
key signature" in
musical notation
Musical notation is any system used to visually represent music. Systems of notation generally represent the elements of a piece of music that are considered important for its performance in the context of a given musical tradition. The proce ...
.
A signature consists of a
set of
data type
In computer science and computer programming, a data type (or simply type) is a collection or grouping of data values, usually specified by a set of possible values, a set of allowed operations on these values, and/or a representation of these ...
s, known as
sorts, together with a
family
Family (from ) is a Social group, group of people related either by consanguinity (by recognized birth) or Affinity (law), affinity (by marriage or other relationship). It forms the basis for social order. Ideally, families offer predictabili ...
of sets, each set containing
operation symbols (or simply symbols) that relate the sorts.
We use
to denote the set of operation symbols relating the sorts
to the sort
.
For example, for the signature of
integer
An integer is the number zero (0), a positive natural number (1, 2, 3, ...), or the negation of a positive natural number (−1, −2, −3, ...). The negations or additive inverses of the positive natural numbers are referred to as negative in ...
stacks, we define two sorts, namely,
and
, and the following family of operation symbols:
::
where
denotes the
empty string
In formal language theory, the empty string, or empty word, is the unique String (computer science), string of length zero.
Formal theory
Formally, a string is a finite, ordered sequence of character (symbol), characters such as letters, digits ...
.
Set-theoretic interpretation of signature
An
algebra
Algebra is a branch of mathematics that deals with abstract systems, known as algebraic structures, and the manipulation of expressions within those systems. It is a generalization of arithmetic that introduces variables and algebraic ope ...
interprets the sorts and operation symbols as sets and
functions.
Each sort
is interpreted as a set
, which is called the carrier of
of sort
, and each symbol
in
is mapped to a function
, which is called an
operation of
.
With respect to the signature of integer stacks, we interpret the sort
as the set
of integers, and interpret the sort
as the set
of integer stacks. We further interpret the family of operation symbols as the following functions:
::
Semantics
Semantics
Semantics is the study of linguistic Meaning (philosophy), meaning. It examines what meaning is, how words get their meaning, and how the meaning of a complex expression depends on its parts. Part of this process involves the distinction betwee ...
refers to the
meaning or
behavior
Behavior (American English) or behaviour (British English) is the range of actions of Individual, individuals, organisms, systems or Artificial intelligence, artificial entities in some environment. These systems can include other systems or or ...
. An algebraic specification provides ''both'' the meaning and behavior of the
object in question.
Equational axioms
The semantics of an algebraic specifications is defined by
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 or ...
s in the form of
conditional equation
In mathematics, an equation is a mathematical formula that expresses the equality of two expressions, by connecting them with the equals sign . The word ''equation'' and its cognates in other languages may have subtly different meanings; for ...
s.
[
With respect to the signature of integer stacks, we have the following axioms:
::For any and ,
::::
::where "" indicates "not found".
]
Mathematical semantics
The mathematical semantics (also known as denotational semantics
In computer science, denotational semantics (initially known as mathematical semantics or Scott–Strachey semantics) is an approach of formalizing the meanings of programming languages by constructing mathematical objects (called ''denotations'' ...
) of a specification refers to its mathematical meaning.
The mathematical semantics of an algebraic specification is the class
Class, Classes, or The Class may refer to:
Common uses not otherwise categorized
* Class (biology), a taxonomic rank
* Class (knowledge representation), a collection of individuals or objects
* Class (philosophy), an analytical concept used d ...
of all algebras that satisfy the specification.
In particular, the classic approach by Goguen et al.[ takes the ]initial algebra
In mathematics, an initial algebra is an initial object in the Category (mathematics), category of F-algebra, -algebras for a given endofunctor . This initiality provides a general framework for mathematical induction, induction and recursion.
...
( unique up to isomorphism
In mathematics, an isomorphism is a structure-preserving mapping or morphism between two structures of the same type that can be reversed by an inverse mapping. Two mathematical structures are isomorphic if an isomorphism exists between the ...
) as the "most representative" model of the algebraic specification.
Operational semantics
The operational semantics of a specification means how to interpret it as a sequence of computational steps.
We define a ground term
In mathematical logic, a ground term of a formal system is a term that does not contain any variables. Similarly, a ground formula is a formula that does not contain any variables.
In first-order logic with identity with constant symbols a ...
as an algebraic expression without variables. The operational semantics of an algebraic specification refers to how ground terms can be transformed using the given equational axioms as left-to-right rewrite rules, until such terms reach their normal forms, where no more rewriting is possible.
Consider the axioms for integer stacks. Let "" denote "rewrites to".
::
Canonical property
An algebraic specification is said to be confluent (also known as Church-Rosser) if the rewriting of any ground term leads to the same normal form. It is said to be terminating if the rewriting of any ground term will lead to a normal form after a finite number of steps. The algebraic specification is said to be canonical (also known as convergent) if it is both confluent and terminating. In other words, it is canonical if the rewriting of any ground term leads to a unique normal form after a finite number of steps.
Given any canonical algebraic specification, the mathematical semantics ''agrees'' with the operational semantics.
As a result, canonical algebraic specifications have been widely applied to address program correctness issues. For example, numerous researchers have applied such specifications to the testing of observational equivalence of objects in object-oriented programming
Object-oriented programming (OOP) is a programming paradigm based on the concept of '' objects''. Objects can contain data (called fields, attributes or properties) and have actions they can perform (called procedures or methods and impl ...
. See Chen and Tse as a secondary source that provides a historical review of prominent research from 1981 to 2013.
See also
* Algebraic semantics (mathematical logic)
* OBJ (programming language) OBJ is a programming language family introduced by Joseph Goguen in 1976, and further worked on by Jose Meseguer.
Overview
It is a family of declarative programming, declarative "ultra high-level" languages. It features Abstract data type, abstract ...
* Joseph Goguen
References
Formal methods
Logic in computer science
Formal specification languages
Programming language semantics