- Algebraic specification
Algebraic specification [cite book|title=Algebraic Specification|first=J. A.|last=Bergstra|coauthors=B. Mahr|publisher=Academic Press|date=1989|isbn=0-201-41635-2] [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] [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] is a formal process of refining specifications to systematically develop more efficient programs.The purpose of an algebraic specification is to
1. represent mathematical structures and functions over those
2. while abstracting from implementation details such as the size of representations (in memory) andthe efficiency of obtaining outcome of computations
3. as such formalizing computations on data
4. allowing for automation due to a limited set of rulesAn algebraic specification achieves these goals by means of defining a number of sorts (data types) togetherwith a collection of functions on them. These functions can usually be divided into two classes:1. constructor functions: these are introduced to create elements of the sort or to construct complexelements from simpler ones.2. 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 thatcase 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 consideredan additional function.In the context of the description of state and state change one may think of the sort as the set of possiblestates (not necessarily all of them can occur in practice) and one may think of the functions as being usefulfor describing the state changes that may occur.It is directly applicable tocomputer science .References:
*Donald Sannella
*Andrzej Tarlecki ee also
*
Common Algebraic Specification Language .
*Formal specification Notes
Wikimedia Foundation. 2010.
