Algebraic specification

Algebraic specification[1][2][3][4] is a software engineering technique for formally specifying system behavior.

Overview

Algebraic specification seeks to systematically develop more efficient programs by:

  1. formally defining types of data, and mathematical operations on those data types
  2. abstracting implementation details, such as the size of representations (in memory) and the efficiency of obtaining outcome of computations
  3. formalizing the computations and operations on data types
  4. allowing for automation by formally restricting operations to this limited set of behaviors and data types.

An algebraic specification achieves these goals by defining one or more data types, and specifying a collection of functions that operate on those data types. These functions can be divided into two classes:

  1. constructor functions: functions that create or initialize the data elements, or construct complex elements from simpler ones
  2. additional functions: functions that operate on the data types, and are defined in terms of the constructor functions.

Example

Consider a formal algebraic specification for the boolean data type.

One possible algebraic specification may provide two constructor functions for the data-element: a true constructor and a false constructor. Thus, a boolean data element could be declared, constructed, and initialized to a value. In this scenario, all other connective elements, such as XOR and AND, would be additional functions. Thus, a data element could be instantiated with either "true" or "false" value, and additional functions could be used to perform any operation on the data element.

Alternatively, the entire system of boolean data types could be specified using a different set of constructor functions: a false constructor and a not constructor. In that case, an additional function could be defined to yield the value "true."

The algebraic specification therefore describes all possible states of the data element, and all possible transitions between states.

gollark: Time to maintain a fork of WE with the "fix" fixed!
gollark: `Sphagnum, Horatio Phillips-Eiffel (1289) On the construction of passages between disjoint locations. Unorthodox Mathematics Monthly 22781 pp. 12-27.` says it is right thus it cannot be wrong.
gollark: æ stupid embeds not working.
gollark: https://wikimedia.org/api/rest_v1/media/math/render/svg/9480572a575787e9ba36b2668328734298a421aa
gollark: WRONG! It is https://wikimedia.org/api/rest_v1/media/math/render/svg/9480572a575787e9ba36b2668328734298a421aa.

See also

Notes
  1. Ehrig, H.; B. Mahr (1989). Algebraic Specification. Academic Press. ISBN 0-201-41635-2.
  2. Bergstra, J.A.; J. Heering; J. Klint (1985). Algebraic Specification. EATCS Monographs on Theoretical Computer Science. 6. Springer-Verlag.
  3. Wirsing, M. (1990). Jan van Leeuwen (ed.). Algebraic Specification. Handbook of Theoretical Computer Science. B. Elsevier. pp. 675–788.
  4. Sannella, Donald; Andrzej Tarlecki (2012). Foundations of Algebraic Specification and Formal Software Development. EATCS Monographs on Theoretical Computer Science. Springer-Verlag. ISBN 978-3-642-17335-6.


This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.