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 Applied science, practical discipli ...

, algebraic semantics 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 Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set ...

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 Reason is the capacity of consciously applying logic by drawing conclusions from new or existing information, with the aim of seeking the truth. It is closely associated with such characteristically human activities as philosophy, science, langu ...

about program specifications in a formal manner.

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 Algebraic specification is a software engineering technique for formally specifying system behavior. It was a very active subject of computer science research around 1980. Overview Algebraic specification seeks to systematically develop more effic ...

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 la, signare, "to sign") is a Handwriting, handwritten (and often Stylization, stylized) 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 ...

of an algebraic specification defines its formal syntax. The word "signature" is used like the concept of "

key signature In Western musical notation, a key signature is a set of sharp (), flat (), or rarely, natural () symbols placed on the staff at the beginning of a section of music. The initial key signature in a piece is placed immediately after the clef a ...

" in

musical notation Music notation or musical notation is any system used to visually represent aurally perceived music played with instruments or sung by the human voice through the use of written, printed, or otherwise-produced symbols, including notation f ...

. A signature consists of a

set Set, The Set, SET or SETS may refer to: Science, technology, and mathematics Mathematics *Set (mathematics), a collection of elements *Category of sets, the category whose objects and morphisms are sets and total functions, respectively Electro ...

S

data type In computer science and computer programming, a data type (or simply type) is a set of possible values and a set of allowed operations on it. A data type tells the compiler or interpreter how the programmer intends to use the data. Most progra ...

s, known as sorts, together with a

family Family (from la, familia) is a group of people related either by consanguinity (by recognized birth) or affinity (by marriage or other relationship). The purpose of the family is to maintain the well-being of its members and of society. Idea ...

\Sigma

of sets, each set containing operation symbols (or simply symbols) that relate the sorts. We use

\Sigma_

to denote the set of operation symbols relating the sorts

s_1,~s_2,~...,~s_n \in S

to the sort

s \in S

. For example, for the signature of

integer An integer is the number zero (), a positive natural number (, , , etc.) or a negative integer with a minus sign ( −1, −2, −3, etc.). The negative numbers are the additive inverses of the corresponding positive numbers. In the languag ...

stacks, we define two sorts, namely,

int

and

stack

, and the following family of operation symbols: ::

\begin
\Sigma_ & = \ \\
\Sigma_ & = \ \\   
\Sigma_ & = \ \\
\Sigma_ & = \ \\
\end

where

\Lambda

denotes the

empty string In formal language theory, the empty string, or empty word, is the unique string of length zero. Formal theory Formally, a string is a finite, ordered sequence of characters such as letters, digits or spaces. The empty string is the special c ...

Set-theoretic interpretation of signature

A

interprets the sorts and operation symbols as sets and functions. Each sort

s

is interpreted as a set

A_s

, which is called the carrier of

A

of sort

s

, and each symbol

\sigma

\Sigma_

is mapped to a function

\sigma_A : A_ \times A_ \times~... \times~A_

, which is called an

operation Operation or Operations may refer to: Arts, entertainment and media * ''Operation'' (game), a battery-operated board game that challenges dexterity * Operation (music), a term used in musical set theory * ''Operations'' (magazine), Multi-Man ...

A

. With respect to the signature of integer stacks, we interpret the sort

int

as the set

\Z

of integers, and interpret the sort

stack

as the set

Stack

of integer stacks. We further interpret the family of operation symbols as the following functions: ::

\begin
 & : ~ \to Stack \\
 & : ~ \Z \times Stack \to Stack \\
 & : ~ Stack \to Stack \\
 & : ~ Stack \to \Z \\
 & : ~ Stack \to \Z \\
\end

Semantics

Semantics Semantics (from grc, σημαντικός ''sēmantikós'', "significant") is the study of reference, meaning, or truth. The term can be used to refer to subfields of several distinct disciplines, including philosophy, linguistics and comput ...

refers to the meaning or

behavior Behavior (American English) or behaviour (British English) is the range of actions and mannerisms made by individuals, organisms, systems or artificial entities in some environment. These systems can include other systems or organisms as we ...

. An algebraic specification provides ''both'' the meaning and behavior of the

object Object may refer to: General meanings * Object (philosophy), a thing, being, or concept ** Object (abstract), an object which does not exist at any particular time or place ** Physical object, an identifiable collection of matter * Goal, an ...

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 Conditional (if then) may refer to: *Causal conditional, if X then Y, where X is a cause of Y *Conditional probability, the probability of an event A given that another event B has occurred *Conditional proof, in logic: a proof that asserts a co ...

equation In mathematics, an equation is a 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 example, in F ...

s. With respect to the signature of integer stacks, we have the following axioms: ::For any

z \in \Z

and

s \in Stack

, ::::

\begin
& A1: ~~  ( (z, s)) = s \\
& A2: ~~  ( (z, s)) =  (s) + 1 \\
& A3: ~~  ( (z, s)) = z \\
& A4: ~~  () =  \\
& A5: ~~  () = 0 \\
& A6: ~~  (s) = -404 ~  (s) = 0 \\
\end

::where "

-404

" 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 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 differently ...

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 of -algebras for a given endofunctor . This initiality provides a general framework for induction and recursion. Examples Functor Consider the endofunctor sending ...

( unique up to

isomorphism In mathematics, an isomorphism is a structure-preserving mapping 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 them. The word i ...

) as the "most representative" model of the algebraic specification.

Operational semantics

The

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 ...

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, the sentence Q(a) \lor P(b ...

as an

algebraic expression In mathematics, an algebraic expression is an expression built up from integer constants, variables, and the algebraic operations (addition, subtraction, multiplication, division and exponentiation by an exponent that is a rational number). ...

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 rule In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or reduc ...

s, until such terms reach their normal forms, where no more rewriting is possible. Consider the axioms for integer stacks. Let "

\Rrightarrow

" denote "rewrites to". ::

\begin
&  ( ( ( (1,~ (2,~ (3,~ ()))))))
& \\
\Rrightarrow ~
&  ( ( ( (1,~ (2,~ (3,~))))))
& ( A4) \\
\Rrightarrow ~
&  ( ( (2,~ (3,~))))
& ( A1) \\
\Rrightarrow ~
&  ( (3,~))
& ( A1) \\
\Rrightarrow ~
& 3
& ( A3) \\
\end

Canonical property

An algebraic specification is said to be

confluent In geography, a confluence (also: ''conflux'') occurs where two or more flowing bodies of water join to form a single channel. A confluence can occur in several configurations: at the point where a tributary joins a larger river (main stem); o ...

(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 The adjective canonical is applied in many contexts to mean "according to the canon" the standard, rule or primary source that is accepted as authoritative for the body of knowledge or literature in that context. In mathematics, "canonical examp ...

(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 An examination (exam or evaluation) or test is an educational assessment intended to measure a test-taker's knowledge, skill, aptitude, physical fitness, or classification in many other topics (e.g., beliefs). A test may be administered verba ...

observational equivalence Observational equivalence is the property of two or more underlying entities being indistinguishable on the basis of their observable implications. Thus, for example, two scientific theories are observationally equivalent if all of their empirically ...

objects Object may refer to: General meanings * Object (philosophy), a thing, being, or concept ** Object (abstract), an object which does not exist at any particular time or place ** Physical object, an identifiable collection of matter * Goal, an ai ...

object-oriented programming Object-oriented programming (OOP) is a programming paradigm based on the concept of "objects", which can contain data and code. The data is in the form of fields (often known as attributes or ''properties''), and the code is in the form of ...

. See Chen and Tse as a

secondary source In scholarship, a secondary sourcePrimary, secondary and tertiary sources
. ...

that provides a historical review of prominent research from 1981 to 2013.

References

Formal methods Logic in computer science Formal specification languages Programming language semantics