алгоритмы, алгебраическая спецификация

[SergeyKostichev]

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

Один из примеров, но мне это вообще ни о чем не говорит, как это читать, как это писать...

adt intset;

sorts intset, int, bool;

ops empty: -> intset;
insert: intset x int -> intset;
delete: intset x int -> intset;
contains: intset x int -> bool;
isempty: intset -> bool;

axioms
insert (insert(x,i),i) = insert (x,i)
delete (empty, i) = empty
delete (insert(x,i),i) = x
delete (insert(x,j),i) = insert (delete(x,i),j)
.
.
.
end intset;

[george66]

А поместите это в раздел computer science - может, там подскажут.

[arseniiv]

Читается это довольно просто, а вот специфическую литературу не помню.

Сначала, видимо, просто описывают название АТД. Оно дальше никак не используется (логичнее считать, что используется $\mathrm{intset}$, которое $\mathbf{sort}$ ниже) и написано либо для возможности ссылаться на этот «модуль» целиком где-то дальше, либо потому что писавшему хотелось какого-то замыкания и он стеснялся без; математически этот заголовок не имеет никакой ценности.

Дальше описываются сорты значений, которые нужны для описания операций, позволяемых над этим АТД. Скорее всего, вы знакомы с типами значений в программировании, вот тут это одно и то же (если и есть какие-то отличия, в этом фрагменте их нельзя усмотреть). Описаны, как можно видеть, сорт объектов самого АТД $\mathrm{intset}$ и сорты целых чисел $\mathrm{int}$ и логических значений $\mathrm{bool}$.

Дальше идёт описание сигнатур/заголовков/типов операций — называть могут по-разному, но в сущности здесь говорится, аргументы каких типов операции принимают и какого типа значения возвращают. (И вы зря выделили названия операций $\mathrm{insert},\ldots,\mathrm{isempty}$ как ключевые слова.) Например, $\mathrm{insert}\colon\mathrm{intset}\times\mathrm{int}\to\mathrm{intset}$ должно означать, что принимаются $\mathrm{intset}$ и $\mathrm{int}$ и выдаётся $\mathrm{intset}$ — как в математической записи определения функции, и функция это и есть (а сорты можно понимать как множества); по смыслу же, очевидно, $\mathrm{intset}(x, i)$ должно означать множество, полученное из $x$ добавлением $i$. Попробуйте с остальными (их смысл должен однозначно восстанавливаться из аксиом, даже если его не описали неформально где-то перед этим определением).

И в конце мы видим аксиомы, говорящие, какой у операций смысл. Например, если добавить в множество два раза подряд один и тот же элемент, это должно быть то же самое, что добавить в него элемент один раз. Это перевод аксиомы $\mathrm{insert}(\mathrm{insert}(x, i), i) = \mathrm{insert}(x, i)$. Попробуйте с остальными тоже.

SergeyKostichev в сообщении #1392834 писал(а):

как это писать

Скорее всего никакого стандарта наподобие UML для описания АТД нет. Когда дело доходит до их реализации, всё пишется уже в терминах конкретного языка, а когда нужны теоретические изыскания, то по-хорошему авторы или ссылаются на схему, которую используют, или описывают её на месте хотя бы рукомахательно, или надеются на то, что читатель более-менее в теме и поймёт, чему какая конструкция должна соответствовать. Автор же вашего курса скорее всего должен был сделать первое или второе, потому что третье было бы нечестно — и если ничего совсем нашлось, мои соболезнования.

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

(Оффтоп)

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

UPD: ещё немного поредактировал-подобавлял.

-- Вт май 14, 2019 21:50:12 --

SergeyKostichev в сообщении #1392834 писал(а):

empty: -> intset

Да, ещё вот это место наверняка может запутать. Тут написано, если математически, либо что $\mathrm{empty}\colon\{()\}\to\mathrm{intset}$, где $\{()\}$ — это множество, содержащее кортеж нулевой длины, либо что $\mathrm{empty}\colon\mathrm{intset}$ (более традиционно это $\mathrm{empty}\in\mathrm{intset}$) — это или нульместная функция с типом результата $\mathrm{intset}$, либо константа такого типа; это одно и то же, и можно видеть, что в аксиомах используется $\mathrm{empty}$ без пустых скобок, но вообще они могли бы там быть.

-- Вт май 14, 2019 21:52:18 --

arseniiv в сообщении #1393002 писал(а):

а вот специфическую литературу не помню

С другой стороны если в некоторой книге есть хотя бы раздел или глава, посвящённые только АТД, там наверняка будет введена какая-то нотация типа той, что выше. Поищите книги, в названии которых упоминается АТД, вдруг найдётся что.

[iifat]

arseniiv в сообщении #1393002 писал(а):

в терминах конкретного языка

Возможно, это уже и есть некий язык. Что-то такое припоминается, вот только вспомнить конретно не могу.