Алгебраическая спецификация

Алгебраическая спецификация - это метод разработки программного обеспечения для формального определения поведения системы.

• 1 Обзор
• 2 Пример
• 3 См. Также
• 4 Примечания

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

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

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

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

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

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

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

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

• Язык общей алгебраической спецификации
• Формальная спецификация
• OBJ

.