Sémantique algébrique (informatique)

In computer science, algebraic semantics is a form of axiomatic semantics based on algebraic laws for describing and reasoning about program specifications in a formal manner. The syntax 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. The signature of an algebraic specification defines its formal syntax. The word "signature" is used like the concept of "key signature" in musical notation. A signature consists of a set of data types, known as sorts, together with a family 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 stacks, we define two sorts, namely, and , and the following family of operation symbols: where denotes the empty string. An algebra 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 refers to the meaning or behavior. An algebraic specification provides both the meaning and behavior of the object in question. The semantics of an algebraic specifications is defined by axioms in the form of conditional equations. With respect to the signature of integer stacks, we have the following axioms: For any and , where "" indicates "not found". The mathematical semantics (also known as denotational semantics) of a specification refers to its mathematical meaning. The mathematical semantics of an algebraic specification is the class of all algebras that satisfy the specification. In particular, the classic approach by Goguen et al.