Algebraic Specification: Difference between revisions
No edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
{{TOCright}}'''Algebraic specification''' <ref>{{cite book|title=Algebraic Specification|first=J. A.|last=Bergstra|coauthors=B. Mahr|publisher=Academic Press|date=1989|isbn=0-201-41635-2}}</ref><ref>{{cite book|title=Algebraic Specification|first=E.|last=Ehrig|coauthors=J. Heering, J. Klint|publisher=Springer-Vrlag|date=1985|series=EATCS Monographs on Theoretical Computer Science|volume=6}}</ref><ref>{{cite book|title=Algebraic Specification|first=M.|last=Wirsing|series=Handbook of Theoretical Computer Science|volume=B|editor=J. van Leeuwen (ed.)|date=1990|publisher=Elsevier|pages=675–788}}</ref> is a specific approach to the formal specification, prototyping, and general development of computer programs. | {{TOCright}}'''Algebraic specification''' <ref name="BHK">{{cite book|title=Algebraic Specification|first=J. A.|last=Bergstra|coauthors=B. Mahr|publisher=Academic Press|date=1989|isbn=0-201-41635-2}}</ref><ref>{{cite book|title=Algebraic Specification|first=E.|last=Ehrig|coauthors=J. Heering, J. Klint|publisher=Springer-Vrlag|date=1985|series=EATCS Monographs on Theoretical Computer Science|volume=6}}</ref><ref>{{cite book|title=Algebraic Specification|first=M.|last=Wirsing|series=Handbook of Theoretical Computer Science|volume=B|editor=J. van Leeuwen (ed.)|date=1990|publisher=Elsevier|pages=675–788}}</ref> is a specific approach to the formal specification, prototyping, and general development of computer programs. | ||
== | == Overview == | ||
As an area of applied mathematics and computer science, algebraic specification addresses these concerns<ref name="BHK"/>: | |||
* | * | ||
Revision as of 05:03, 22 July 2009
Algebraic specification [1][2][3] is a specific approach to the formal specification, prototyping, and general development of computer programs.
Overview
As an area of applied mathematics and computer science, algebraic specification addresses these concerns[1]:
-
- represent applications and their subparts as mathematical objects and functions applicable to same
- abstract from implementation details irrelevant to the mathematics of the application
- formalizing computations for specific data models
- provide opportunities for automation due to a now explicit rule base embodied in the theory which the specification embodies
Implementation
An algebraic specification achieves these goals by means of defining a number of sorts (data types) together
with a collection of functions on them. These functions can usually be divided into two classes:
- constructor functions: these are introduced to create elements of the sort or to construct complex elements from simpler ones.
- additional functions: these are functions defined in terms of the constructor functions.
If one considers an algebraic specification of the Booleans the constructors can be true and false. In that
case all other connectives, such as ^ and _, may be considered to be additional functions. Alternatively,
also the combination of false and ¬ can be considered constructors. In that case true may be considered
an additional function.
In the context of the description of state and state change one may think of the sort as the set of possible
states (not necessarily all of them can occur in practice) and one may think of the functions as being useful
for describing the state changes that may occur.
Researchers
See also
Notes
- ↑ 1.0 1.1 Bergstra, J. A.; B. Mahr (1989). Algebraic Specification. Academic Press. ISBN 0-201-41635-2.
- ↑ Ehrig, E.; J. Heering, J. Klint (1985). Algebraic Specification. EATCS Monographs on Theoretical Computer Science. 6. Springer-Vrlag.
- ↑ Wirsing, M. (1990). J. van Leeuwen (ed.). ed. Algebraic Specification. Handbook of Theoretical Computer Science. B. Elsevier. pp. 675–788.
