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

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

Обзор

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

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

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

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

Примеры

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

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

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

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

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

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

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

            (1 - (1 - p)) = p
      ((1 - (n - p)) - 1) = (p - n)
  ((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))
  ...

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

См. также

Примечания

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

[1] Эриг, Хартмут ; Махр, Бернд (1989). Алгебраическая спецификация . Академическая пресса. ISBN 0-201-41635-2 .

[2] Бергстра, Дж.А.; Хиринг, Дж.; Клинт, Дж. (1985). Алгебраическая спецификация . Монографии EATCS по теоретической информатике. Том. 6. Шпрингер-Верлаг.

[3] Вирсинг, Мартин (1990). Ян ван Леувен (ред.). Алгебраическая спецификация . Справочник по теоретической информатике. Том. Б. Эльзевир. стр. 675–788.

[4] Саннелла, Дональд; Тарлецкий, Анджей (2012). Основы алгебраической спецификации и формальной разработки программного обеспечения . Монографии EATCS по теоретической информатике. Спрингер-Верлаг. ISBN 978-3-642-17335-6 .

[5] Вагнер, Эрик Г. (декабрь 2002 г.). «Алгебраические спецификации: немного старой истории и новые мысли» . Северный журнал вычислительной техники . 9 (4): 373–404. ISSN 1236-6064 .

[1]

[2]

[3]

[4]

[5]