Алгебраическая спецификация - Википедия - Algebraic specification

Алгебраическая спецификация[1][2][3][4] это метод разработки программного обеспечения для формально определяя поведение системы.

Обзор

Алгебраическая спецификация направлена ​​на систематическую разработку более эффективных программ путем:

  1. формально определяющий типы данных, и математические операции с этими типами данных
  2. абстрагирование деталей реализации, таких как размер представлений (в памяти) и эффективность получения результата вычислений
  3. формализация вычислений и операций над типами данных
  4. возможность автоматизации путем формального ограничения операций этим ограниченным набором поведений и типов данных.

Алгебраическая спецификация достигает этих целей, определяя один или несколько типов данных и указывая набор функций, которые работают с этими типами данных. Эти функции можно разделить на два класса:

  1. функции конструктора: функции, которые создают или инициализируют элементы данных или создают сложные элементы из более простых
  2. дополнительные функции: функции, которые работают с типами данных и определены в терминах функций-конструкторов.

Пример

Рассмотрим формальную алгебраическую спецификацию для логический тип данных.

Одна возможная алгебраическая спецификация может предоставлять две функции-конструкторы для элемента данных: истинный конструктор и ложный конструктор. Таким образом, логический элемент данных может быть объявлен, сконструирован и инициализирован значением. В этом сценарии все остальные соединительные элементы, Такие как XOR и И, было бы дополнительные функции. Таким образом, элемент данных может быть создан со значением «истина» или «ложь», а дополнительные функции могут использоваться для выполнения любой операции с элементом данных.

В качестве альтернативы вся система логических типов данных может быть указана с использованием другого набора функций-конструкторов: ложный конструктор и нет конструктор. В этом случае можно определить дополнительную функцию для получения значения «истина».

Следовательно, алгебраическая спецификация описывает все возможные состояния элемента данных, и все возможные переходы между штатами.

Смотрите также

Примечания

  1. ^ Ehrig, H .; Б. Мар (1989). Алгебраическая спецификация. Академическая пресса. ISBN  0-201-41635-2.
  2. ^ Bergstra, J.A .; Дж. Херинг; Дж. Клинт (1985). Алгебраическая спецификация. Монографии EATCS по теоретической информатике. 6. Springer-Verlag.
  3. ^ Вирсинг, М. (1990). Ян ван Леувен (ред.). Алгебраическая спецификация. Справочник по теоретической информатике. B. Эльзевир. С. 675–788.
  4. ^ Саннелла, Дональд; Анджей Тарлецкий (2012). Основы алгебраической спецификации и формальной разработки программного обеспечения. Монографии EATCS по теоретической информатике. Springer-Verlag. ISBN  978-3-642-17335-6.