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

Материал из eSyr's wiki.

Перейти к: навигация, поиск

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

Текущая версия Ваш текст
Строка 16: Строка 16:
Методика — вещь более размытая. Например, есть методика взятия интегралов? Вообще, есть, вас ей учили на первых курсах.
Методика — вещь более размытая. Например, есть методика взятия интегралов? Вообще, есть, вас ей учили на первых курсах.
-
Больше общих требований нет, и в реальной жизни методологий по построению программ, отвечающих всем трём позициям, нет. И то, что мы будем рассматривать, достаточно общие решения, но не нужно ждать от них фантастических результатов.
+
Больше у лектора общих требований нет, и в реальной жизни методологий по построению программ, отвечающих всем трём позициям, нет. И то, что мы будем рассматривать, достаточно общие решения, но не нужно ждать от них фантастических результатов.
VDM. Откуда растут корни?
VDM. Откуда растут корни?
Строка 28: Строка 28:
Рассмотрим пример.
Рассмотрим пример.
-
Мы уже не раз проходили, как устроена ОС, знаем, что процессы переходят из одних состояний в другие: например, iowait, пассивные. Это достаточно формальное определение, конечный автомат, и будем считать, что больше ничего нет. Микроядерная ОС (mm и pm) — порядка 10 строчек на С. Как проверить соответствие?
+
Мы уже не раз проходили, как устроена ОС, знаем, что процессы переходят из одних состояний в другие: например, iowait, пассивные. Это достаточно формальное определение, конечный автомат, и будем считать, что больше ничего нет. Микроядерная ОС (mm и pm) --- порядка 10 строчек на С. Как проверить соответствие?
Например, проверить все переходы и состояния. Да, но этот подход недостаточно технологичный. Хотелось бы некое общее состояние получить.
Например, проверить все переходы и состояния. Да, но этот подход недостаточно технологичный. Хотелось бы некое общее состояние получить.
 +
 +
Лектор не на 100% уверен, ...
Общий подход следующий: мы разделяем два мира: мир моделей и реализаций. В модели и реализации, и там и там, есть своё пространство составляющих. Для простоты будем считать, что есть операции, функции, и данные берутся из входного пространства данных и данные генерируются в выходное пространство данных. Эти пространства разные. И в случае модели есть такая структура данных, пис. конечный автомат. В программе реализации такой может не быть. Там могут быть структуры существенно более богатые. И имеются операции. И тогда для проверки корректности рисуется такая диаграмма: имеется некоторое состояние, и мы в этом состоянии i_model мы применяем к нему переход f_модель и получаем результат j_model. И можем сделать соответствие i_impl →(f_impl) j_impl. Заметьте, что, собственно, входные данные не просто разные, но и в разных пространствах лежат. Между ними надо и можно установить соответствие. Соответствие устанавливается в эту сторону. Это некое отображение от сложного к простому. Часто это отображение называют абстракцией. Более принятое название — функция retrieve, retr. Коротко и красиво что можно сказать: реализация корректна в том и только в том случае, если диаграмма коммутативна.
Общий подход следующий: мы разделяем два мира: мир моделей и реализаций. В модели и реализации, и там и там, есть своё пространство составляющих. Для простоты будем считать, что есть операции, функции, и данные берутся из входного пространства данных и данные генерируются в выходное пространство данных. Эти пространства разные. И в случае модели есть такая структура данных, пис. конечный автомат. В программе реализации такой может не быть. Там могут быть структуры существенно более богатые. И имеются операции. И тогда для проверки корректности рисуется такая диаграмма: имеется некоторое состояние, и мы в этом состоянии i_model мы применяем к нему переход f_модель и получаем результат j_model. И можем сделать соответствие i_impl →(f_impl) j_impl. Заметьте, что, собственно, входные данные не просто разные, но и в разных пространствах лежат. Между ними надо и можно установить соответствие. Соответствие устанавливается в эту сторону. Это некое отображение от сложного к простому. Часто это отображение называют абстракцией. Более принятое название — функция retrieve, retr. Коротко и красиво что можно сказать: реализация корректна в том и только в том случае, если диаграмма коммутативна.
Строка 54: Строка 56:
Был выдвинут тезис, что модель и retr должны быть адекватны, и это правильно. Но с другой стороны, если модель большая, то приходится сильнее абстрагироваться.
Был выдвинут тезис, что модель и retr должны быть адекватны, и это правильно. Но с другой стороны, если модель большая, то приходится сильнее абстрагироваться.
-
Основная сложность — в функции retr. Сложность retr фактически сложность реализации. Поэтому подход другой: строится цепочка моделей. Для компиляторов было порядка 5 или 6 этапов.
+
Основная сложность --- в функции retr. Сложность retr фактически сложность реализации. Поэтому подход другой: строится цепочка моделей. Для компиляторов было порядка 5 или 6 этапов.
При помощи VDM верифицировали компилятор Ada.
При помощи VDM верифицировали компилятор Ada.
Строка 60: Строка 62:
Многие противники подхода говорили: вместо того, чтобы сделать работу честно и правильно 1 раз, необходимо сделать её несколько раз, провести работу по доказательству (которая очень трудоёмкая). Но опыт показал, что на компиляторах сроки разработки удаётся сократить и удаётся предъявить корректную программу с первого предъявления.
Многие противники подхода говорили: вместо того, чтобы сделать работу честно и правильно 1 раз, необходимо сделать её несколько раз, провести работу по доказательству (которая очень трудоёмкая). Но опыт показал, что на компиляторах сроки разработки удаётся сократить и удаётся предъявить корректную программу с первого предъявления.
-
Товарищи, которые разработали VDM... RAISE расшифровывается как строгий подход к программной инженерии (rational approach to software engineering). Чтобы этим требованиям удовлетворять, самую сложную технологическую деталь в технологии VDM решили убрать — retr. Чем retr был хорош? Можно было изменять сигнатуру функции. VDM всё это разрешал, а RAISE запретил. что осталось? остался подход пошаговой детализации. Поскльку retr убрали, то сигнатуры модели и реализации совпали, структуры данных по существу одни и те же, т.к. что всё сильно упростилось, но при этом raise отошёл на ещё один шаг назад. Что было в VDM? Пусть в VDM первая модель — эксплицитная функция. При этом структуры данных должны быть описаны и заданы. В случае с нашим конечным автоматом разработчик может уже задуматься, как хранить состояние. Разработчики сказали, что на первом этапе модель должна быть предельно абстрактной. Функции есть, структур нет. И этот способ описания поведения системы, когда сигнатуры операций задаются, стр. не задаются, называют аксиоматической или алгебраической спецификацией. Есть тонкости в трактовке (кс и алг), но для нас разницы нет. В RAISE были введены аксиомы и при помощи них это опис.
+
Товарищи, которые разработали VDM... RAISE расшифровывается как строгий подход к программной инженерии (rational approach to software engineering). Чтобы этим требованиям удовлетворять, самую сложную технологическую деталь в технологии VDM решили убрать --- retr. Чем retr был хорош? Можно было изменять сигнатуру функции. VDM всё это разрешал, а RAISE запретил. что осталось? остался подход пошаговой детализации. Поскльку retr убрали, то сигнатуры модели и реализации совпали, структуры данных по существу одни и те же, т.к. что всё сильно упростилось, но при этом raise отошёл на ещё один шаг назад. Что было в VDM? Пусть в VDM первая модель --- эксплицитная функция. При этом структуры данных должны быть описаны и заданы. В случае с нашим конечным автоматом разработчик может уже задуматься, как хранить состояние. Разработчики сказали, что на первом этапе модель должна быть предельно абстрактной. Функции есть, структур нет. И этот способ описания поведения системы, когда сигнатуры операций задаются, стр. не задаются, называют аксиоматической или алгебраической спецификацией. Есть тонкости в трактовке (кс и алг), но для нас разницы нет. В RAISE были введены аксиомы и при помощи них это опис.
И при помощи RAISE может расписать достаточно детально:
И при помощи RAISE может расписать достаточно детально:
Строка 77: Строка 79:
1.4 Доказательство согласованности.
1.4 Доказательство согласованности.
-
Модели 0 и 1 уровня должны быть согласованы. Как это делается. Согласованность с позиции RSL термин неформальный, а технология RAISE ... расматривается отношение уточнения, дана модель мдет уточн. другую, и мы можем считать что модель 1 уточняет модель 0, если одна уточняет другую. И уточняет, если всё сохраняется и добавлено только новое, и есть один нюанс, связанный с уточнением самих типов данных. До этого типы данных были представлены только именами, по мере того, как прибл. к реализации, мы в какой-то момент, не обязательно для всех типов одновременно, должны эти типы определить (списки, деревья....) переходят объявления к определению можно делать два раза, не более чем. Первый раз — берётся и пис. реальная структура (например T3 — натуральное число или T4 — список натуральных чисел). Могу уточнить (T4 — конечный список натуральных чисел). Это первое уточнение типа. Второй вид: для каждой стр. данных форм. определяется т. н. максимальный тип. Это некий тип., пр. природу. Для булевских чисел максимальных. типов вл. сами булевские числа. Для натуральных — целые. Для конечных списков, множеств, тобр — бесконечн. Если есть список натуральных чисел, то вопрос, что будет максимальным типом стр. данных, гр. список натуральных чисел? Бесконечный список целых чисел. Такое уточнение — максимизация — тоже правильное уточнение. Самое главное, что нужно доказать — все аксиомы сохраняются.
+
Модели 0 и 1 уровня должны быть согласованы. Как это делается. Согласованность с позиции RSL термин неформальный, а технология RAISE ... расматривается отношение уточнения, дана модель мдет уточн. другую, и мы можем считать что модель 1 уточняет модель 0, если одна уточняет другую. И уточняет, если всё сохраняется и добавлено только новое, и есть один нюанс, связанный с уточнением самих типов данных. До этого типы данных были представлены только именами, по мере того, как прибл. к реализации, мы в какой-то момент, не обязательно для всех типов одновременно, должны эти типы определить (списки, деревья....) переходят объявления к определению можно делать два раза, не более чем. Первый раз — берётся и пис. реальная структура (например T3 — натуральное число или T4 --- список натуральных чисел). Могу уточнить (T4 --- конечный список натуральных чисел). Это первое уточнение типа. Второй вид: для каждой стр. данных форм. определяется т. н. максимальный тип. Это некий тип., пр. природу. Для булевских чисел максимальных. типов вл. сами булевские числа. Для натуральных --- целые. Для конечных списков, множеств, тобр --- бесконечн. Если есть список натуральных чисел, то вопрос, что будет максимальным типом стр. данных, гр. список натуральных чисел.? Бесконечный список целых чисел. Такое уточнение --- максимизация --- тоже правильное уточнение. Самое главное, что нужно доказать --- все аксиомы сохраняются.
Техника доказательства достаточно простая и очевидная, как правило, подстановка. Дост.ю просто делать, если была аксиматическая спецификация, а в модели 1 написали определение. Помимо подст. исп. библиотек правил вывода, а она связ. с теориями, пстр. для типовых структур данных. Например: в случае множеств в теории сказано, что x ∈ {} всегда тождественно равно false. И при помощи последнего упрощения должны прийти к тому, что либо все аксиомы тождественно true, либо где-то не true, и вы доказали, что новая спецификация не является строгим уточнением исходной. В этом и состоит метод.
Техника доказательства достаточно простая и очевидная, как правило, подстановка. Дост.ю просто делать, если была аксиматическая спецификация, а в модели 1 написали определение. Помимо подст. исп. библиотек правил вывода, а она связ. с теориями, пстр. для типовых структур данных. Например: в случае множеств в теории сказано, что x ∈ {} всегда тождественно равно false. И при помощи последнего упрощения должны прийти к тому, что либо все аксиомы тождественно true, либо где-то не true, и вы доказали, что новая спецификация не является строгим уточнением исходной. В этом и состоит метод.
Строка 113: Строка 115:
Теперь грустном: на экзамене будет задача, на которой необходимо будет доказать правильности или неправильность уточнения.
Теперь грустном: на экзамене будет задача, на которой необходимо будет доказать правильности или неправильность уточнения.
-
По поводу реальной жизни: никакие подобные системы аналитически не заказываются, на отдельные подсистемы техника доказательства используется в RAISE. Тематика становится всё более востребованной.
+
По поводу реальной жизни: никакие подобные системы аналитически не заказываются, на отдельные подсистемы техн. доказ, исп. в raise, также исп. Тематика становится всё более востребованной.
{{МФСП}}
{{МФСП}}
{{Lection-stub}}
{{Lection-stub}}

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!


Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Получено с http://esyr.org/wiki/%D0%9C%D0%A4%D0%A1%D0%9F%2C_03_%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F_%28%D0%BE%D1%82_17_%D1%81%D0%B5%D0%BD%D1%82%D1%8F%D0%B1%D1%80%D1%8F%29
Личные инструменты
Разделы