- •Математическая индукция. Принципы простой индукции, модифицированной простой индукции, строгой индукции.
- •1) Доказать, что справедливо s(1);
- •Основные принципы доказательства правильности для блок-схем с использованием индукции. Инварианты цикла при доказательстве правильности.
- •Метод индуктивных утверждений как обобщение метода доказательства правильности с использованием индукции. Верификация программ.
- •Метод индуктивных утверждений.
- •Метод индуктивных утверждений
- •Надежность программных средств
- •Доказательство правильности программы
- •Формализация доказательства с помощью индуктивных утверждений. Множество условий верификации.
- •Аксиоматический подход к доказательству частичной правильности и его идентичность методу индуктивных утверждений.
- •Рекурсивные программы. Доказательство их правильности методом структурной индукции. Рекурсия
- •Метод структурной индукции
- •Моделирование. Природа моделируемых систем. Применение теории сетей Петри. Прикладная и чистая теории сетей Петри.
- •Структура сетей Петри. Способы задания сетей Петри. Графы сетей Петри.
- •Маркировка сетей Петри. Правила выполнения сетей Петри. Пространство состояний сетей Петри.
- •События и условия. Моделирование процесса сетью Петри. Примитивные и непримитивные события. Одновременность и конфликт.
- •Сети Петри для моделирования. Моделирование аппаратного обеспечения сетями Петри (конечные автоматы, эвм с конвейерной обработкой, кратные функциональные блоки).
- •Сети Петри для моделирования. Моделирование программного обеспечения сетями Петри (блок-схемы, обеспечение параллелизма).
- •Сети Петри в решении задач синхронизации: задача о взаимном исключении, задача о производителе/потребителе, задача об обедающих мудрецах, задача о чтении/записи, p- и V-системы и др.
- •Задачи анализа сетей Петри: безопасность, ограниченность, сохранение, активность, покрываемость.
- •Дерево достижимости сети Петри.
- •Использование дерева достижимости для анализа сетей Петри.
- •Матричные уравнения и их использование для анализа сетей Петри.
- •Сети Петри с ограничениями и подклассы сетей Петри.
- •1) Автоматные сети Петри
- •2) Маркированные графы
- •3) Сети свободного выбора
- •4) Правильные сети Петри
- •Расширенные модели сетей Петри (области ограничения, переходы исключающее или, сети со сдерживающими дугами, сети с приоритетами, временные сети)
- •Взаимосвязь мощности моделирования и мощности разрешения сетей Петри
Метод индуктивных утверждений как обобщение метода доказательства правильности с использованием индукции. Верификация программ.
Верификация (подтверждение правильности) – состоит в проверке и доказательстве корректности разработанной программы по отношению к совокупности формальных утверждений, представленных в спецификации и полностью определяющей связь между входными и выходными данными этой программы. При этом отношения между переменными н входе и выходе программы анализируется не в виде значений, как при тестировании, а в виде описаний их свойств, проявляющихся при любых процессах обработок этих переменных контролируемой в программе.
Верификация программы в принципе исключает необходимость её тестирования и отладки, так как при этом на более высоком уровне понятий и описаний всех переменных, устанавливается корректность процессов, их обработка и преобразования.
Сущность каждой программы можно представить описаниями отношений между входными и выходными данными. Эти отношения формализуются 1 программной спецификации. В реальных разработках формализация этих взаимосвязей является неплохой, и часть отношений уточняется в процессе разработок программ. Такие не полностью определённые недостаточны для доказательства корректности программ. Только при полной и точной формализации всех условий и связей между входными и результирующими данными появляется возможность их использования для автоматической верификации.
Метод индуктивных утверждений.
Для изучения этого метода программа снабжается утверждениями о свойствах её переменных в нкоторых точках:
a) Входные переменные не меняются в процессе исполнения программ;
b) Описываются состояния переменных в промежуточных точках;
c) Выходные переменные описываются с помощью отношениями между переменными после завершения программы.
Верификация состоит в последовательной демонстрации того, что из входных переменных и преобразований, выполненных на первом шаге следует истинность утверждения, сформированного в следующей промежуточной точке.
Для верификации программ необходимо три языка:
Язык записи текстов программ;
Язык формулировки условий верификации;
Язык формирования и доказательства корректности.
Так как эти языки различаются в значительной степени, то это обстоятельство является одним из применения верификации.
Доказательство корректности имеет следующие преимущества:
1. Представляет собой чёткий формализованный процесс.
2. Требует анализа. Процесс доказательства корректности дает возможность рассматривать части программ, которое в противном случае анализируется лишь случайно.
3. проясняет промежуточные результаты вычислений. Выписывании выражений заставляет программиста четко сформировать свои предположения о результатах вычислений в выбранных точках программы.
4. Выявляет зависимости. В процессе доказательства программ начинает понимать какие предположения о входных данных не явно испытывается в различных частях программы.
Недостатки метода:
1. Сложность; даже для небольших простых программ выкладки очень сложны, что может привести к ошибкам.
2. Ошибки, Из-за сложности метода легко допустить ошибки и при формировании доказываемых утверждений и при доказательстве.
3. Трудности работы с массивами.
4. Отсутствие мощного математического аппарата.
5. Высокая трудоёмкость. Для проверки программы требуется затраты труда, чем для её написания (в 2 – 6 раз).
6. Отсутствие выразительности. Часто нелегко сформировать выгодно утверждение для того что интуитивно представляется очень простым вычислением:
7. Трудность понимания.
8. Необходимость обучения. Для применении этого метода требуется длительное обучение и тренировка.