Algebraic Specification: Difference between revisions

From Cibernética Americana
Jump to navigationJump to search
No edit summary
No edit summary
Line 2: Line 2:
<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=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>
<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 formal specification of computer programs.
is a specific approach to formal specification of computer programs.
== Goals ==
== Goals ==
The purpose of an algebraic specification is to:<br />
The purpose of an algebraic specification is to:<br />
1. represent mathematical structures and functions over those<br />
 
2. while abstracting from implementation details such as the size of representations (in memory) and the efficiency of obtaining outcome of computations<br />
# represent mathematical structures and functions over those<br />
3. as such formalizing computations on data<br />
# while abstracting from implementation details such as the size of representations (in memory) and the efficiency of obtaining outcome of computations<br />
4. allowing for automation due to a limited set of rules<br /><br />
# as such formalizing computations on data<br />
#. allowing for automation due to a limited set of rules<br /><br />
 
An algebraic specification achieves these goals by means of defining a number of sorts (data types) together
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:<br />
with a collection of functions on them. These functions can usually be divided into two classes:<br />
1. constructor functions: these are introduced to create elements of the sort or to construct complex
 
elements from simpler ones.<br />
#. constructor functions: these are introduced to create elements of the sort or to construct complex
2. additional functions: these are functions defined in terms of the constructor functions.
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
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,
case all other connectives, such as ^ and _, may be considered to be additional functions. Alternatively,

Revision as of 11:57, 21 July 2009

Algebraic specification [1][2] [3] is a specific approach to formal specification of computer programs.

Goals

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) and the efficiency of obtaining outcome of computations
  3. as such formalizing computations on data
  4. . allowing for automation due to a limited set of rules

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:

  1. . constructor functions: these are introduced to create elements of the sort or to construct complex

elements from simpler ones.

  1. . 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.
It is directly applicable to computer science.

Researchers

See also

Notes

  1. Bergstra, J. A.; B. Mahr (1989). Algebraic Specification. Academic Press. ISBN 0-201-41635-2. 
  2. Ehrig, E.; J. Heering, J. Klint (1985). Algebraic Specification. EATCS Monographs on Theoretical Computer Science. 6. Springer-Vrlag. 
  3. Wirsing, M. (1990). J. van Leeuwen (ed.). ed. Algebraic Specification. Handbook of Theoretical Computer Science. B. Elsevier. pp. 675–788. 

Template:Compsci-stub