Algebraic specification

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 to computer science.

References:
* Donald Sannella
* Andrzej Tarlecki

ee also

* Common Algebraic Specification Language.
* Formal specification

Notes


Wikimedia Foundation. 2010.

Игры ⚽ Поможем сделать НИР

Look at other dictionaries:

  • Common Algebraic Specification Language — The Common Algebraic Specification Language (CASL) is a general purpose specification language based on first order logic with induction. Partial functions and subsorting are also supported. CASL has been designed by CoFI, the Common Framework… …   Wikipedia

  • Algebraic notation (chess) — Algebraic notation Algebraic notation (or AN) is a method for recording and describing the moves in a game of chess. It is now standard among all chess organizations and most books, magazines, and newspapers. In English speaking countries, AN… …   Wikipedia

  • Algebraic chess notation — is used to record and describe the moves in a game of chess. It is now standard among all chess organizations and most books, magazines, and newspapers. In English speaking countries, it replaced the parallel system of descriptive chess notation …   Wikipedia

  • Specification language — A specification language is a formal language used in computer science.Unlike most programming languages, which are directly executable formal languages used to implement a system, specification languages are used during systems analysis,… …   Wikipedia

  • Formal specification — A formal specification is a mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not (necessarily) how the system should do it. Given such a specification, it is… …   Wikipedia

  • Model-based specification — is an approach to formal specification where the system specification is expressed as a system state model. This state model is constructed using well understood mathematical entities such as sets and functions. System operations are specified by …   Wikipedia

  • Standard Algebraic Notation — Portable Game Notation Pour les articles homonymes, voir PGN. Portable Game Notation (PGN) désigne un standard de codage des parties d échecs. Il est principalement utilisé pour la retransmission des parties sur internet et dans les bases de… …   Wikipédia en Français

  • Jan Bergstra — Jan A Bergstra is a Dutch computer scientist. His work has focussed on logic and the theoretical foundations of software engineering, especially on formal methods for system design. He is best known as an expert on algebraic methods for the… …   Wikipedia

  • Larch family — The Larch family of formal specification languages are intended for the precise specification of computing systems. They allow the clean specification of computer programs and the formulation of proofs about program behavior.The Larch family was… …   Wikipedia

  • Methode formelle (informatique) — Méthode formelle (informatique) Pour les articles homonymes, voir Méthode. En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l aide de logique mathématique, sur des programmes informatiques ou… …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”