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

Алгебраическая спецификация ^{[1] [2] [3] [4]} — это метод разработки программного обеспечения для формального описания поведения системы. Это был очень активный предмет исследований в области компьютерных наук около 1980 года. ^[5]

Обзор

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

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

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

1. Функции конструктора : Функции, которые создают или инициализируют элементы данных или создают сложные элементы из более простых. Набор доступных функций конструктора подразумевается сигнатурой спецификации . Кроме того, спецификация может содержать уравнения , определяющие эквивалентности между объектами, созданными этими функциями. Является ли базовое представление идентичным для различных, но эквивалентных конструкций, зависит от реализации.
2. Дополнительные функции : функции, которые работают с типами данных и определяются в терминах функций конструктора.

Примеры

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

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

В качестве альтернативы, вся система булевых типов данных может быть определена с использованием другого набора функций-конструкторов: конструктор false и конструктор not . В этом случае можно определить дополнительную функцию true для получения значения not false , и следует добавить уравнение . ${\displaystyle ({\text{not}}\;{\text{not}}\;x)=x}$

Таким образом, алгебраическая спецификация описывает все возможные состояния элемента данных и все возможные переходы между состояниями. ^{[ необходима ссылка ]}

Для более сложного примера целые числа можно указать (помимо многих других способов, выбрав один из многочисленных формализмов) с помощью двух конструкторов

 1 : Я (_ - _) : Z × Z -> Z

и три уравнения:

 (1 - (1 - п)) = п ((1 - (н - п)) - 1) = (п - п) ((p1 - n1) - (n2 - p2)) = (p1 - (n1 - (p2 - n2))

Легко проверить, что уравнения верны, учитывая обычную интерпретацию двоичной функции «минус». (Имена переменных были выбраны так, чтобы намекнуть на положительный и отрицательный вклад в значение.) Приложив немного усилий, можно показать, что, применяемые слева направо, они также образуют конфлюэнтную и завершающую систему переписывания, отображающую любой сконструированный термин в однозначную нормальную форму, представляющую соответствующее целое число:

 ... (((1 - 1) - 1) - 1) ((1 - 1) - 1) (1 - 1) 1 (1 - ((1 - 1) - 1)) (1 - (((1 - 1) - 1) - 1)) ...

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

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

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

Примечания

1. Эхриг, Хартмут ; Махр, Бернд (1989). Алгебраическая спецификация . Academic Press. ISBN 0-201-41635-2.
2. Бергстра, JA; Хиринг, Дж.; Клинт, Дж. (1985). Алгебраическая спецификация . Монографии EATCS по теоретической информатике. Том 6. Springer-Verlag.
3. Вирсинг, Мартин (1990). Ян ван Леувен (ред.). Алгебраическая спецификация . Справочник по теоретической информатике. Т. B. Elsevier. С. 675–788.
4. Саннелла, Дональд; Тарлецки, Анджей (2012). Основы алгебраической спецификации и формальной разработки программного обеспечения . Монографии EATCS по теоретической информатике. Springer-Verlag. ISBN 978-3-642-17335-6.
5. Вагнер, Эрик Г. (декабрь 2002 г.). «Алгебраические спецификации: немного старой истории и новых мыслей». Nordic Journal of Computing . 9 (4): 373–404. ISSN  1236-6064.