Конспект лекций по предмету "Надежность систем"

Узнать цену работы по вашей теме


Характеристика формальных методов доказательства

Наиболее известными формальными методами доказательства программ являются метод рекурсивной индукции или утверждений Флойда, Наура, метод структурной индукции Хоара и др. [6.4, 6.5, 6.18, 6.19].
Метод Флойда основан на определении условий для входных и выходных данных и в выборе контрольных точек в доказываемой программе так, чтобы путь прохождения по программе пересекал хотя бы одну контрольную точку. Для этих точек формулируются утверждения о состоянии и значениях переменных в них (для циклов эти утверждения должны быть истинными при каждом прохождении циклаинварианта).
Каждая точка рассматривается для индуктивного утверждения того, что формула остается истинной при возвращении в эту точку программы и зависит не только от входных и выходных данных, но и от значений промежуточных переменных. На основе индуктивных утверждений и условий на аргументы создаются утверждения с условиями проверки правильности программы в отдельных ее точках. Для каждого пути программы между двумя точками устанавливается проверка на соответствие условий правильности и определяется истинность этих условий при успешном завершении программы на данных, удовлетворяющих входным условиям.
Формирование таких утверждений - довольно сложная задача, особенно для программ с высокой степенью параллельности и взаимодействия с пользователем. Кроме того, трудно проверить достаточность и правильность самих утверждений.
Доказательство корректности применялось для уже написанных программ и тех, которые разрабатываются методом последовательной декомпозиции задачи на подзадачи, для каждой из них формулируются утверждения с учетом условий ввода и вывода и точек программы, расположенными между входными и выходными утверждениями. Суть доказательства истинности выполнения условий и утверждений относительно заданной программы и составляет основу доказательства ее правильности.
Данный метод доказательства уменьшает число ошибок и время тестирования программы, обеспечивает отработку спецификаций программы на полноту, однозначность и непротиворечивость.
Метод Хоара- это усовершенствованный метод Флойда, основанный на аксиоматическом описании семантики языка программирования исходных программ. Каждая аксиома описывает изменение значений переменных с помощью операторов этого языка. Формализация операторов перехода и вызовов процедур обеспечивается с помощью правил вывода, содержащих индуктивные высказывания для каждой точки и функции исходной программы.
Система правил вывода дополняется механизмом переименования глобальных переменных, условиями на аргументы и результаты, а также на правильность задания данных программы. Оператор перехода трактуется как выход из циклов и аварийных ситуаций.
Описание с помощью системы правил утверждений - громоздкое и отличается неполнотой, поскольку все правила предусмотреть невозможно. Данный метод проверялся экспериментально на множестве программ без применения средств автоматизации из-за их отсутствия.
Метод Маккартисостоит в структурной проверке функций, работающих над структурными типами данных, структур данных и диаграмм перехода во время символьного выполнения программ. Эта техника включает в себя моделирование выполнения кода с использованием символов для изменяемых данных. Тестовая программа имеет входное состояние, данные и условия ее выполнения.
Выполняемая программа рассматривается как серия изменений состояний. Самое последнее состояние программы считается выходным состоянием и если оно получено, то программа считается правильной. Данный метод обеспечивает высокое качество исходного кода.
Метод Дейкстрыпредлагает два подхода к доказательству правильности программ. Первый подход основан на модели вычислений, оперирующей с историями результатов вычислений программы, анализом путей прохождения и правил обработки большого объема информации. Второй подход базируется на формальном исследовании текста программы с помощью предикатов первого порядка. В процессе выполнения программа получает некоторое состояние, которое запоминается для дальнейших сравнений.
Основу метода составляет математическая индукция, абстрактное описание программы и ее вычисление. Математическая индукция применяется при прохождении циклов и рекурсивных процедур, а также необходимых и достаточных условий утверждений. Абстракция позволяет сформулировать некоторые количественные ограничения. При вычислении на основе инвариантных отношений проверяются на правильность границы вычислений и получаемые результаты.
Процесс формального доказательства правильности программ методом математической индукции зарекомендовал себя как система правил статической проверки правильности программ за столом для обнаружения в них формальных ошибок. С помощью этого метода можно доказать истинность некоторого предположения в зависимости от параметра для всех , и тем самым доказать случай . Исходя из истинности для любого значения , доказывается , что достаточно для доказательства истинности для всех .
Путь доказательства следующий. Пусть даны описание некоторой правильной программы (ее логики) и утверждение относительно этой программы, которая при выполнении достигает некоторой определенной точки. Проходя через эту точку раз, можно получить справедливость утверждения , если индуктивно доказать, что:
1. справедливо при первом проходе через заданную точку,
2. если справедливо при проходах через заданную точку, то справедливо и прохождение через заданную точку раз.
Исходя из предположения, что программа в конце концов успешно завершится, утверждение о ее правильности будет справедливым.


Не сдавайте скачаную работу преподавателю!
Данный конспект лекций Вы можете использовать для создания шпаргалок и подготовки к экзаменам.

Доработать Узнать цену работы по вашей теме
Поделись с друзьями, за репост + 100 мильонов к студенческой карме :

Пишем конспект самостоятельно:
! Как написать конспект Как правильно подойти к написанию чтобы быстро и информативно все зафиксировать.

Другие популярные конспекты:

Конспект Основные проблемы и этапы развития средневековой философии
Конспект Проблема познаваемости мира. Гносеологический оптимизм, скептицизм, агностицизм. Взаимосвязь субъекта и объекта познания
Конспект Понятие финансовой устойчивости организации
Конспект Внутренняя политика первых Романовых.
Конспект Понятие мировоззрения, его уровни и структура. Исторические типы мировоззрения
Конспект ПРОБЛЕМЫ КВАЛИФИКАЦИИ ПРЕСТУПЛЕНИЙ
Конспект Синтагматические, парадигматические и иерархические отношения в языке
Конспект Тема 1.2. Плоская система сходящихся сил. Определение равнодействующей геометрическим способом 13
Конспект Происхождение человека. Основные концепции антропосоциогенеза. Антропогенез и культурогенез.
Конспект Общая характеристика процессов сбора, передачи, обработки и накопления информации