Редактирование: МФСП, 03 лекция (от 17 сентября)

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

Мы уже не раз проходили, как устроена ОС, знаем, что процессы переходят из одних состояний в другие: например, iowait, пассивные. Это достаточно формальное определение, конечный автомат, и будем считать, что больше ничего нет. Микроядерная ОС (mm и pm) — порядка 10 строчек на С. Как проверить соответствие?

Общий подход следующий: мы разделяем два мира: мир моделей и реализаций. В модели и реализации, и там и там, есть своё пространство составляющих. Для простоты будем считать, что есть операции, функции, и данные берутся из входного пространства данных и данные генерируются в выходное пространство данных. Эти пространства разные. И в случае модели есть такая структура данных, пис. конечный автомат. В программе реализации такой может не быть. Там могут быть структуры существенно более богатые. И имеются операции. И тогда для проверки корректности рисуется такая диаграмма: имеется некоторое состояние, и мы в этом состоянии i_model мы применяем к нему переход f_модель и получаем результат j_model. И можем сделать соответствие i_impl →(f_impl) j_impl. Заметьте, что, собственно, входные данные не просто разные, но и в разных пространствах лежат. Между ними надо и можно установить соответствие. Соответствие устанавливается в эту сторону. Это некое отображение от сложного к простому. Часто это отображение называют абстракцией. Более принятое название — функция retrieve, retr. Коротко и красиво что можно сказать: реализация корректна в том и только в том случае, если диаграмма коммутативна.

<math>\forall i\_impl \isin i\_impl := pre\_model (retr(i\_impl)) \rArr pre\_impl (i\_impl)</math>

Этот подход в общем смысле формален, т.к.: предусловие может слаб. модель. По поводу постусловия обратная ситуация.

Что реально нужно делать, чтобы доказывать корректность программ: RAISE очень похож на VDM. Спец. опис. реальным, рзм или имплицитным. Retr представляется как обычная функция, и потом просто нужно уметь доказывать, что два retr выполняются.

Основная сложность — в функции retr. Сложность retr фактически сложность реализации. Поэтому подход другой: строится цепочка моделей. Для компиляторов было порядка 5 или 6 этапов.

Товарищи, которые разработали VDM... RAISE расшифровывается как строгий подход к программной инженерии (rational approach to software engineering). Чтобы этим требованиям удовлетворять, самую сложную технологическую деталь в технологии VDM решили убрать — retr. Чем retr был хорош? Можно было изменять сигнатуру функции. VDM всё это разрешал, а RAISE запретил. что осталось? остался подход пошаговой детализации. Поскльку retr убрали, то сигнатуры модели и реализации совпали, структуры данных по существу одни и те же, т.к. что всё сильно упростилось, но при этом raise отошёл на ещё один шаг назад. Что было в VDM? Пусть в VDM первая модель — эксплицитная функция. При этом структуры данных должны быть описаны и заданы. В случае с нашим конечным автоматом разработчик может уже задуматься, как хранить состояние. Разработчики сказали, что на первом этапе модель должна быть предельно абстрактной. Функции есть, структур нет. И этот способ описания поведения системы, когда сигнатуры операций задаются, стр. не задаются, называют аксиоматической или алгебраической спецификацией. Есть тонкости в трактовке (кс и алг), но для нас разницы нет. В RAISE были введены аксиомы и при помощи них это опис.

И при помощи RAISE может расписать достаточно детально:

0.1 Определяются некие типы данных. Не описываются, а просто объявляются.

0.2 Описываются сигнатуры операций (функций). Это значит, во-первых, задаётся имя функции и перечисляются типы операндов и результата (входных и выходных данных)

0.2.1 С точки зрения RAISE, константы это такая функция без значений

Они указывают, что функция тотальна, детерминирована и терминирующ. Если функция нетотальная, то надо писать тильду. На уровне сигнатур в чём нетотальность определить нельзя, надо смотреть сигнатуру

1.1 Типы данных можно пополнить.

1.3 Можно пополнить набор аксиом. Но все старые аксимы сохранятся.

1.4 Доказательство согласованности.

Модели 0 и 1 уровня должны быть согласованы. Как это делается. Согласованность с позиции RSL термин неформальный, а технология RAISE ... расматривается отношение уточнения, дана модель мдет уточн. другую, и мы можем считать что модель 1 уточняет модель 0, если одна уточняет другую. И уточняет, если всё сохраняется и добавлено только новое, и есть один нюанс, связанный с уточнением самих типов данных. До этого типы данных были представлены только именами, по мере того, как прибл. к реализации, мы в какой-то момент, не обязательно для всех типов одновременно, должны эти типы определить (списки, деревья....) переходят объявления к определению можно делать два раза, не более чем. Первый раз — берётся и пис. реальная структура (например T3 — натуральное число или T4 — список натуральных чисел). Могу уточнить (T4 — конечный список натуральных чисел). Это первое уточнение типа. Второй вид: для каждой стр. данных форм. определяется т. н. максимальный тип. Это некий тип., пр. природу. Для булевских чисел максимальных. типов вл. сами булевские числа. Для натуральных — целые. Для конечных списков, множеств, тобр — бесконечн. Если есть список натуральных чисел, то вопрос, что будет максимальным типом стр. данных, гр. список натуральных чисел? Бесконечный список целых чисел. Такое уточнение — максимизация — тоже правильное уточнение. Самое главное, что нужно доказать — все аксиомы сохраняются.

Техника доказательства достаточно простая и очевидная, как правило, подстановка. Дост.ю просто делать, если была аксиматическая спецификация, а в модели 1 написали определение. Помимо подст. исп. библиотек правил вывода, а она связ. с теориями, пстр. для типовых структур данных. Например: в случае множеств в теории сказано, что x &isin; {} всегда тождественно равно false. И при помощи последнего упрощения должны прийти к тому, что либо все аксиомы тождественно true, либо где-то не true, и вы доказали, что новая спецификация не является строгим уточнением исходной. В этом и состоит метод.

Пример: полностью пример имеется в методическом пособии.

Других ксим рассматривать не будем.

Эт нулевой уровень спецификации на первом обязаны пост. все спец. сигн, но БД, например, будет уточнена

Проверяем. Все типы данных определены, все сигнатуры пр. Для одного типа данных сказали, что это мн-во пар, и для двух функций сказали, что empty всегда даёт пустое множество, и функция defined определена таким утверждением. Этого достаточно, чтобы рассуждать о сохранении или несохранении аксиомы. Для того, чтобы это делать, есть некая техника. В простом случае мы просто раскрываем все кванторы.

Раскрываем &forall;, defined, empty, потом раскручиваем квантор существования и мы приходим к некоторому выражению: (k, d) &isin; {}. Мы знаем, что это false, это означает, что левая часть тождественно false, значит, аксиома тождественно true. Вот мы провели доказательство, что первая аксиома сохранилась.

Практик-еор сообр: как в общем случае проверять? общего ответа нет. Какие вообще спец. включать, а какие нет? В общем случае ответа на этот вопрос нет. Практический подход такой: в наших функциях мы делаем первое грубое разделение: какие функции сзд. новые данные в нашей системе (тут мы уже разделяем целевые объекты и вспомогательные). Те операции, где мы получаем новое состояние БД, это т.н. функции-генераторы, генераторы новых значений целевого типа. Те функции, которые позволяют узнать только некоторые характеристики, это некие обсерверы, которые позволяют что-то узнать (напр, lookup). Эти функции на состояние БД не влияют. И есть ещё более тонкое деление: функция remove. Любое значение Database мною построено при помощи цепочки инсертов, и для генерации всех значений БД куьщму не нужна, а а в реальной жизни нужна и в модели должна присутствовать. Эти функции, которые несут некоторую избыточность, их называют трансформерами или модификаторами. Они меняют состояние, но они приводят к состояниям, к которым можно без них перейти.

В число аксиом системы обычно включают аксиомы, описывающие генераторы и обсерверы. А после того, как отработал генератор или трансформер, как изменилось поведение системы? А это даёт обсервера. И если для комбинаторной генерации и обс. есть опис. поведение, то это даёт эффект генератора. Т.о., мы должны согласовать с лектором, это самое абсолютное описание системы, которое может быть.

Теперь грустном: на экзамене будет задача, на которой необходимо будет доказать правильности или неправильность уточнения.

По поводу реальной жизни: никакие подобные системы аналитически не заказываются, на отдельные подсистемы техника доказательства используется в RAISE. Тематика становится всё более востребованной.