HOME

TheInfoList



OR:

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 S 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 ...
\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 (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, 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 (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 ...
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 in \Sigma_ is mapped to a function \sigma_A : A_ \times A_ \times~... \times~A_, which is called an operation of 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 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 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, 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 "\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 (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