请输入您要查询的百科知识:

 

词条 Algebraic specification
释义

  1. Example

  2. See also

  3. Notes

Algebraic specification,[1][2][3] is a software engineering technique for formally specifying system behavior. 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.

See also

  • Common Algebraic Specification Language
  • Donald Sannella
  • Formal specification

Notes

1. ^{{cite book|title=Algebraic Specification|first=H.|last= Ehrig|author2=B. Mahr|publisher=Academic Press|year=1989|isbn=0-201-41635-2}}
2. ^{{cite book|title=Algebraic Specification|first=J.A.|last=Bergstra|author2=J. Heering |author3=J. Klint |publisher=Springer-Verlag|year=1985|series=EATCS Monographs on Theoretical Computer Science|volume=6}}
3. ^{{cite book|title=Algebraic Specification|first=M.|last=Wirsing|series=Handbook of Theoretical Computer Science|volume=B|editor=Jan van Leeuwen|year=1990|publisher=Elsevier|pages=675–788}}
{{compsci-stub}}

1 : Formal methods

随便看

 

开放百科全书收录14589846条英语、德语、日语等多语种百科知识,基本涵盖了大多数领域的百科知识,是一部内容自由、开放的电子版国际百科全书。

 

Copyright © 2023 OENC.NET All Rights Reserved
京ICP备2021023879号 更新时间:2024/11/10 12:41:33