- •Математическая индукция. Принципы простой индукции, модифицированной простой индукции, строгой индукции.
- •1) Доказать, что справедливо s(1);
- •Основные принципы доказательства правильности для блок-схем с использованием индукции. Инварианты цикла при доказательстве правильности.
- •Метод индуктивных утверждений как обобщение метода доказательства правильности с использованием индукции. Верификация программ.
- •Метод индуктивных утверждений.
- •Метод индуктивных утверждений
- •Надежность программных средств
- •Доказательство правильности программы
- •Формализация доказательства с помощью индуктивных утверждений. Множество условий верификации.
- •Аксиоматический подход к доказательству частичной правильности и его идентичность методу индуктивных утверждений.
- •Рекурсивные программы. Доказательство их правильности методом структурной индукции. Рекурсия
- •Метод структурной индукции
- •Моделирование. Природа моделируемых систем. Применение теории сетей Петри. Прикладная и чистая теории сетей Петри.
- •Структура сетей Петри. Способы задания сетей Петри. Графы сетей Петри.
- •Маркировка сетей Петри. Правила выполнения сетей Петри. Пространство состояний сетей Петри.
- •События и условия. Моделирование процесса сетью Петри. Примитивные и непримитивные события. Одновременность и конфликт.
- •Сети Петри для моделирования. Моделирование аппаратного обеспечения сетями Петри (конечные автоматы, эвм с конвейерной обработкой, кратные функциональные блоки).
- •Сети Петри для моделирования. Моделирование программного обеспечения сетями Петри (блок-схемы, обеспечение параллелизма).
- •Сети Петри в решении задач синхронизации: задача о взаимном исключении, задача о производителе/потребителе, задача об обедающих мудрецах, задача о чтении/записи, p- и V-системы и др.
- •Задачи анализа сетей Петри: безопасность, ограниченность, сохранение, активность, покрываемость.
- •Дерево достижимости сети Петри.
- •Использование дерева достижимости для анализа сетей Петри.
- •Матричные уравнения и их использование для анализа сетей Петри.
- •Сети Петри с ограничениями и подклассы сетей Петри.
- •1) Автоматные сети Петри
- •2) Маркированные графы
- •3) Сети свободного выбора
- •4) Правильные сети Петри
- •Расширенные модели сетей Петри (области ограничения, переходы исключающее или, сети со сдерживающими дугами, сети с приоритетами, временные сети)
- •Взаимосвязь мощности моделирования и мощности разрешения сетей Петри
Надежность программных средств
Шуман [5] определяет надежность программных средств как вероятность того, что данная системная программа в течение заданного периода времени будет безошибочно работать на машине, для которой она создана, при условии, что она используется с учетом ее конструктивных возможностей и ограничений. Надежность часто выражается такими количественными показателями, как средняя наработка на отказ и средняя наработка до (первого) отказа, или степень сохранности базы данных. Эти показатели, естественно, в гораздо большей степени применимы к системе, чем к одиночной программе или модулю.
Доказательство правильности программы
В последние несколько лет наблюдается растущий интерес к разработке принципов строгого доказательства правильности программы. Это делается обычно безотносительно к внешним условиям в которых работает программа, с помощью набора определений, аксиом и теорем. Можно надеяться, что со временем будут разработаны методы автоматизации (полной или частичной) процедуры доказательства правильности программы, но пока в этой области еще много нерешенных проблем. Как мы указывали в гл.4, трудность доказательства правильности программы сильно зависит от сложности программы и от числа взаимосвязей между ее компонентами; поэтому на структурное программирование, которое призвано уменьшить сложность программ, возлагаются большие надежды и с точки зрения упрощения процесса доказательства работоспособности программ.
Методы доказательства частичной корректности программ как правило опираются на аксиоматический подход к формализации семантики языков программирования. В настоящее время известны аксиоматические семантики Паскаля, подмножества ПЛ/1 и некоторых других языков.
Аксиоматическая семантика языка программирования представляет собой совокупность аксиом и правил вывода. С помощью аксиом задается семантика простых операторов языка (присваивания, ввода - вывода, вызова процедур). С помощью правил вывода описывается семантика составных операторов или управляющих структур (последовательности, условного выбора, циклов). Среди этих правил вывода надо отметить правило вывода для операторов цикла так как оно требует знания инварианта цикла (формулы, истинности которой не изменяется при любом прохождении цикла).
Построение инварианта для оператора цикла по его тексту является алгоритмически не разрешимой задачи, поэтому для описания семантики циклов требуется своего рода ”подсказка” от разработчика программы.
Наиболее известным из методов доказательства частичной корректности программ является метод индуктивных утверждений предложенный Флойдом и усовершенствованный Хоаром. Метод состоит из трех этапов.
Первый этап - получение аннотированной программы. На этом этапе для синтаксически правильной программы должны быть заданы утверждения на языке логики предикатов первого порядка :
- входной предикат ;
- выходной предикат ;
- по одному утверждению для каждого цикла (эти утверждения задаются для входной точки цикла и должны характеризовать семантику вычислений в цикле).
Доказательство неистинности условий корректности свидетельствует о неправильности программы, или ее спецификации, или программы и спецификации.
Несмотря на достаточную сложность процесса верификации программы и на то, что даже успешно завершенная верификация не дает гарантий качества программы ( т.к. ошибка может содержаться и в верификации ), применение методов аналитического доказательства правильности очень полезно для уточнения смысла разрабатываемой программы, а знание этих методов благотворно сказывается на квалификации программиста.
Наконец, динамический контроль программы - это проверка правильности программы при ее выполнении на компьютере, т.е. тестирование.