Алгебраическая семантика (информатика)

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

Синтаксис

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

Определение подписи

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

Сигнатура состоит из набора типов данных , известных как сортировки , вместе с семейством наборов, каждый из которых содержит символы операций (или просто символы), которые связывают сортировки. Мы используем для обозначения набора символов операций, связывающих сортировки с сортировкой . ${\displaystyle S}$ ${\displaystyle \Sigma }$ ${\displaystyle \Sigma _{s_{1}s_{2}...s_{n},~s}}$ ${\displaystyle s_{1},~s_{2},~...,~s_{n}\in S}$ ${\displaystyle s\in S}$

Например, для сигнатуры целочисленных стеков мы определяем два сорта, а именно и , а также следующее семейство символов операций: ${\displaystyle int}$ ${\displaystyle stack}$

${\displaystyle {\begin{aligned}\Sigma _{\Lambda ,~stack}&=\{{\rm {new}}\}\\\Sigma _{int~stack,~stack}&=\{{\rm {push}}\}\\\Sigma _{stack,~stack}&=\{{\rm {pop}}\}\\\Sigma _{stack,~int}&=\{{\rm {depth}},{\rm {top}}\}\\\end{aligned}}}$

где обозначает пустую строку . ${\displaystyle \Lambda }$

Теоретико-множественная интерпретация сигнатуры

Алгебра интерпретирует символы сортировок и операций как множества и функции . Каждая сортировка интерпретируется как множество , которое называется носителем сортировки , а каждый символ в сопоставляется функции , которая называется операцией . ${\displaystyle A}$ ${\displaystyle s}$ ${\displaystyle A_{s}}$ ${\displaystyle A}$ ${\displaystyle s}$ ${\displaystyle \sigma }$ ${\displaystyle \Sigma _{s_{1}s_{2}...s_{n},~s}}$ ${\displaystyle \sigma _{A}:A_{s_{1}}\times A_{s_{2}}\times ~...\times ~A_{s_{n}}}$ ${\displaystyle A}$

Что касается сигнатуры целых стеков, мы интерпретируем сортировку как набор целых чисел, а сортировку как набор целых стеков. Мы далее интерпретируем семейство символов операций как следующие функции: ${\displaystyle int}$ ${\displaystyle \mathbb {Z} }$ ${\displaystyle stack}$ ${\displaystyle Stack}$

${\displaystyle {\begin{aligned}{\rm {new}}&:~\to Stack\\{\rm {push}}&:~\mathbb {Z} \times Stack\to Stack\\{\rm {pop}}&:~Stack\to Stack\\{\rm {depth}}&:~Stack\to \mathbb {Z} \\{\rm {top}}&:~Stack\to \mathbb {Z} \\\end{aligned}}}$

Семантика

Семантика относится к значению или поведению . Алгебраическая спецификация обеспечивает как значение, так и поведение рассматриваемого объекта .

Эквациональные аксиомы

Семантика алгебраической спецификации определяется аксиомами в форме условных уравнений . ^[1]

Относительно сигнатуры целочисленных стеков имеем следующие аксиомы:

Для любого и , ${\displaystyle z\in \mathbb {Z} }$ ${\displaystyle s\in Stack}$

${\displaystyle {\begin{aligned}&A1:~~{\rm {pop}}({\rm {push}}(z,s))=s\\&A2:~~{\rm {depth}}({\rm {push}}(z,s))={\rm {depth}}(s)+1\\&A3:~~{\rm {top}}({\rm {push}}(z,s))=z\\&A4:~~{\rm {pop}}({\rm {new}})={\rm {new}}\\&A5:~~{\rm {depth}}({\rm {new}})=0\\&A6:~~{\rm {top}}(s)=-404~{\rm {if~depth}}(s)=0\\\end{aligned}}}$

где « » означает «не найдено». ${\displaystyle -404}$

Математическая семантика

Математическая семантика (также известная как денотационная семантика ) ^[5] спецификации относится к ее математическому значению.

Математическая семантика алгебраической спецификации — это класс всех алгебр, которые удовлетворяют спецификации. В частности, классический подход Гогуэна и др. ^{[1] [2]} берет исходную алгебру ( единственную с точностью до изоморфизма ) как «наиболее представительную» модель алгебраической спецификации.

Операционная семантика

Операционная семантика ^[6] спецификации означает, как ее интерпретировать как последовательность вычислительных шагов.

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

Рассмотрим аксиомы для целочисленных стеков. Пусть " " обозначает "переписывает в". ${\displaystyle \Rrightarrow }$

${\displaystyle {\begin{aligned}&{\rm {top}}({\rm {pop}}({\rm {pop}}({\rm {push}}(1,~{\rm {push}}(2,~{\rm {push}}(3,~{\rm {pop}}({\rm {new}})))))))&\\\Rrightarrow ~&{\rm {top}}({\rm {pop}}({\rm {pop}}({\rm {push}}(1,~{\rm {push}}(2,~{\rm {push}}(3,~{\rm {new}}))))))&({\rm {by~Axiom~}}A4)\\\Rrightarrow ~&{\rm {top}}({\rm {pop}}({\rm {push}}(2,~{\rm {push}}(3,~{\rm {new}}))))&({\rm {by~Axiom~}}A1)\\\Rrightarrow ~&{\rm {top}}({\rm {push}}(3,~{\rm {new}}))&({\rm {by~Axiom~}}A1)\\\Rrightarrow ~&3&({\rm {by~Axiom~}}A3)\\\end{aligned}}}$

Каноническое свойство

Алгебраическая спецификация называется конфлюэнтной (также известной как Черч-Россер ), если перезапись любого основного термина приводит к той же нормальной форме. Она называется завершающейся, если перезапись любого основного термина приведет к нормальной форме после конечного числа шагов. Алгебраическая спецификация называется канонической (также известной как сходящейся ), если она является как конфлюэнтной, так и завершающейся. Другими словами, она является канонической, если перезапись любого основного термина приводит к уникальной нормальной форме после конечного числа шагов.

При любой канонической алгебраической спецификации математическая семантика согласуется с операционной семантикой. ^[7]

В результате канонические алгебраические спецификации широко применялись для решения проблем корректности программ. Например, многочисленные исследователи применяли такие спецификации для проверки наблюдательной эквивалентности объектов в объектно -ориентированном программировании . См. Chen and Tse ^[8] в качестве вторичного источника , который предоставляет исторический обзор выдающихся исследований с 1981 по 2013 год.

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

• Алгебраическая семантика (математическая логика)
• OBJ (язык программирования)
• Джозеф Гоген

Ссылки

1. JA Goguen; JW Thatcher; EG Wagner; JB Wright (1977). «Начальная семантика алгебры и непрерывные алгебры». Журнал ACM . 24 (1): 68–95. doi : 10.1145/321992.321997 . S2CID  11060837.
2. JA Goguen ; JW Thatcher ; EG Wagner (1978). «Первоначальный алгебраический подход к спецификации, корректности и реализации абстрактных типов данных». В RT Yeh (ред.). Современные тенденции в методологии программирования, т. IV: Структурирование данных . Prentice Hall . стр. 80–149.
3. JA Goguen ; C. Kirchner; H. Kirchner; A. Megrelis; J. Meseguer (1988). "Введение в OBJ3". Труды первого семинара по системам условной перезаписи терминов . Конспект лекций по информатике. Том 308. Springer . С. 258–263. doi :10.1007/3-540-19242-5_22. ISBN 978-3-540-19242-8.
4. JA Goguen ; G. Malcolm (1996). Алгебраическая семантика императивных программ. MIT Press . ISBN  9780262071727.
5. Дэвид А. Шмидт (1986). Денотационная семантика: методология развития языка . William C. Brown Publishers. ISBN 9780205104505.
6. Гордон Д. Плоткин (1981). «Структурный подход к операционной семантике» (Технический отчет DAIMI FN-19). Кафедра компьютерных наук, Орхусский университет .
7. S. Lucas; J. Meseguer (2014). "Сильное и слабое операционное завершение упорядоченно-сортированных переписывающих теорий". В S. Escobar (ред.). Переписывание логики и ее приложения. Lecture Notes in Computer Science. Vol. 8663. Cham: Springer . pp. 178–194. doi :10.1007/978-3-319-12904-4_10. ISBN 978-3-319-12903-7.
8. HY Chen; TH Tse (2013). «Равенство равным и неравным: пересмотр критериев эквивалентности и неэквивалентности в тестировании объектно-ориентированного программного обеспечения на уровне классов». IEEE Transactions on Software Engineering . 39 (11): 1549–1563. doi : 10.1109/TSE.2013.33. hdl : 10722/187124 . S2CID  8694513.