- •Математическая индукция. Принципы простой индукции, модифицированной простой индукции, строгой индукции.
- •1) Доказать, что справедливо s(1);
- •Основные принципы доказательства правильности для блок-схем с использованием индукции. Инварианты цикла при доказательстве правильности.
- •Метод индуктивных утверждений как обобщение метода доказательства правильности с использованием индукции. Верификация программ.
- •Метод индуктивных утверждений.
- •Метод индуктивных утверждений
- •Надежность программных средств
- •Доказательство правильности программы
- •Формализация доказательства с помощью индуктивных утверждений. Множество условий верификации.
- •Аксиоматический подход к доказательству частичной правильности и его идентичность методу индуктивных утверждений.
- •Рекурсивные программы. Доказательство их правильности методом структурной индукции. Рекурсия
- •Метод структурной индукции
- •Моделирование. Природа моделируемых систем. Применение теории сетей Петри. Прикладная и чистая теории сетей Петри.
- •Структура сетей Петри. Способы задания сетей Петри. Графы сетей Петри.
- •Маркировка сетей Петри. Правила выполнения сетей Петри. Пространство состояний сетей Петри.
- •События и условия. Моделирование процесса сетью Петри. Примитивные и непримитивные события. Одновременность и конфликт.
- •Сети Петри для моделирования. Моделирование аппаратного обеспечения сетями Петри (конечные автоматы, эвм с конвейерной обработкой, кратные функциональные блоки).
- •Сети Петри для моделирования. Моделирование программного обеспечения сетями Петри (блок-схемы, обеспечение параллелизма).
- •Сети Петри в решении задач синхронизации: задача о взаимном исключении, задача о производителе/потребителе, задача об обедающих мудрецах, задача о чтении/записи, p- и V-системы и др.
- •Задачи анализа сетей Петри: безопасность, ограниченность, сохранение, активность, покрываемость.
- •Дерево достижимости сети Петри.
- •Использование дерева достижимости для анализа сетей Петри.
- •Матричные уравнения и их использование для анализа сетей Петри.
- •Сети Петри с ограничениями и подклассы сетей Петри.
- •1) Автоматные сети Петри
- •2) Маркированные графы
- •3) Сети свободного выбора
- •4) Правильные сети Петри
- •Расширенные модели сетей Петри (области ограничения, переходы исключающее или, сети со сдерживающими дугами, сети с приоритетами, временные сети)
- •Взаимосвязь мощности моделирования и мощности разрешения сетей Петри
Метод индуктивных утверждений
Метод индуктивных утверждений независимо сформулирован К. Флойдом и П. Науром. Суть этого метода состоит в следующем:
1) формулируются входное и выходное утверждения: входное утверждение описывает все необходимые входные условия для программы (или программного фрагмента), выходное утверждение описывает ожидаемый результат;
2) предполагая истинным входное утверждение, строится выведенное утверждение, которое выводится на основании семантики операторов, расположенных между входом и выходом (входным и выходным утверждениями);
3) формулируется теорема (условия верификации): из выведенного утверждения следует выходное утверждение;
4) доказывается теорема, что свидетельствует о правильности программы (программного фрагмента).
Пусть А – утверждение, описывающее предполагаемые свойства данных в программе, а С - утверждение, описывающее то, что по предположению требуется получить в результате выполнения программы (утверждение о правильности). Программа частично правильна, если при каждом ее выполнении с данными, удовлетворяющими предположению А, будет справедливо утверждение С при условии, что программа закончится.
Программа полностью правильна, если она частично правильна и заканчивается при всех данных удовлетворяющих предположению А.
Доказательство правильности программ с помощью индуктивных утверждений
Для доказательства частичной правильности свяжем утверждение А с началом программы, а утверждение С с конечной точкой программы. Выявим закономерности, относящиеся к значениям переменных, и свяжем соответствующие утверждения (условия верификации), по крайней мере, с одной из точек в каждом цикле. Для каждого пути в программе, ведущего из точки i, связанной с утверждением Аi, в точку j, связанную с утверждением Аj, (при условии, что на этом пути нет точек с какими-либо дополнительными утверждениями), докажем, что если мы попали в точку i и справедливо с утверждение Аi, а затем прошли от точки i до точки j, то при попадании в точку j будет справедливо с утверждение Аj. Для циклов точки i и j могут быть одной и той же точкой.
Для доказательства полной правильности программы сначала нужно доказать ее частичную правильность, а затем уже доказать, что программа когда-нибудь завершится.
Алгоритм доказательства правильности программы методом индуктивных утверждений :
1) Построить структуру программы.
2) Выписать входное и выходное утверждения.
3) Сформулировать для всех циклов индуктивные утверждения .
4) Составить список выделенных путей.
5) Построить условия верификации.
6) Доказать условие верификации.
7) Доказать, что выполнение программы закончится.
Частичная и полная правильность программы. Теорема о частичной правильности. Доказательство частичной и полной правильности как часть процесса программирования.
Частичная и полная правильность программы
Учитывая специфику появления ошибок в программах в процессе их выполнения на компьютере, целесообразно выделить в понятие "правильность (корректность) программы" два понятия:
(а) "частичная корректность программы" - это удовлетворение спецификациям при условии завершения выполнения программы; (б) "завершение программы" - это достижение в процессе выполнения программы, начатой в допустимом (для входной спецификации) состоянии, выхода программы.
Свойство завершения программы не является тривиальным для такого объекта, как программа, ввиду возможности циклических вычислений, а также наличия частично-определённых операций. Случаи, когда свойство завершения не удовлетворяется, довольно обычны для программ с ошибками, и дают заведомо некорректные программы.
Будем говорить, что программа завершается, если ее выполнение доходит до конца за конечное время и при этом отсутствуют ошибки фазы выполнения. Если выполнение программы приводит к получению правильного результата когда бы она не завершилась, то говорят, что программа является частично правильной (корректной). Если, кроме того, доказывается, что выполнение программы действительно заканчивается, то говорят, что программа является полностью правильной (корректной). Будем говорить, что программа S частично правильна относительно входного условия P и выходного условия Q (что обозначается: {P}S{Q}), если в случае, когда предикат P истинен для входных значений переменных и программа S завершает работу, предикат Q истинен для выходных значений переменных. При этом предикат P называется предусловием программы S, а предикат Q - постусловием программы S. Будем говорить, что программа S является тотально правильной (что обозначается: <P>S<Q>), если программа S частично правильна относительно P и Q, а также программа S завершает работу для входных значений переменных, удовлетворяющих условию P.
Каждое из двух выделенных свойств корректности программы, может удовлетворяться или не удовлетворяться. Таким образом, можно выделить шесть основных задач анализа корректности [:
(1) частичная корректность (при условии завершения); (2) завершение программы; (3) незавершение программы; (4) тотальная корректность (частичная корректность и завершение); (5) частичная некорректность (некорректность при условии завершения); (6) некорректность (незавершение или частичная некорректность).
Отметим, что разделение свойств частичной корректности и завершения следует рассматривать как методологический прием, направленный на уменьшение сложности соответствующих доказательств.
В общей постановке (для произвольных программ) каждое из этих свойств (завершение и частичная корректность) является алгоритмически неразрешимым. Однако для различных классов программ могут быть развиты достаточно эффективные методы анализа свойств корректности, позволяющие вручную или в автоматизированном режиме проводить соответствующие доказательства.