Методы и средства инженерии программного обеспечения



         

Общая характеристика формальных методов доказательства - часть 2


Операторы перехода, рассматриваемый как  выход из  циклов и аварийных ситуаций,   и вызовов процедур  определяются правилами  вывода, каждое из  которых задает индуктивное высказывание для каждой   метки и функции исходной программы Система правил вывода дополняется механизмом  переименования глобальных переменных, условиями на аргументы и результаты.

Метод рекурсивных индукций Дж. Маккарти  состоит в структурной проверке функций, работающих над структурными типами данных,  изменяет структуры данных и диаграммы перехода во время  символьного выполнения программ. Тестовая программа получает детерминированное входное состояние при вводе данных и условий, которое  обеспечивает фиксацию переменных и изменение состояния.

Выполняемая программа рассматривается как серия изменений состояний, самое  последнее состояние считается  выходным состоянием и если оно получено, то программа считается  правильной. Моделирование выполнения кода является  дорогим процессом, обеспечивающим  высокое качество исходного кода.

 

Метод Дейкстры  включает два  подхода к доказательству правильности программ.  Первый – основан на модели вычислений, оперирующих с  историями результатов вычислений  при работе программ и  анализом выполнения  модели вычислений.

Второй подход базируется на формальном исследовании текста программы с помощью предикатов первого порядка применительно к  классу асинхронных программ, в которых возникают  состояния при выполнении операторов. В конце выполнения  программы уничтожаются  накопленные  отработанные состояния программы. Основу этого метода составляет ­ – перевычисление, математическая индукция и абстракция.

Перевычисление базируется на инвариантах отношений, которые проверяют границы вычислений в проверяемой программе. Математическая индукция применяется для проверки циклов и рекурсивных процедур с помощью необходимых и достаточных условий повторения вычислений. Абстракция

задает количественные ограничения, которые накладываются  методом перевычислений.




Содержание  Назад  Вперед