birmaga.ru
добавить свой файл

1

Лекция 6.04.05

На прошлой лекции мы определили два вида корректности.

Частичная корректность:


Полная корректность:


Свойства отношений частичной и полной корректности:

Лемма 1:



Лемма 2:



Лемма 3:



Леммы 2 и 3 также верны и для полной корректности.
Доказать корректность программы – это означает доказать, что некоторая модель программы находится в отношении «удовлетворяет» к некоторой модели требований к этой программе.

Рассмотрим, как доказать, что данная блок схема удовлетворяет условиям спецификации.

Вспомним пример из прошлой лекции. Дана блок схема программы, реализующей целочисленное деление:


Спецификация:





Домены всех переменных – множества целых чисел.

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

Доказательство полной корректности будет разбито на два этапа. Сначала мы докажем, что программа является частично корректной относительно входного и выходного предикатов (используем метод индуктивных утверждений Флойда). А затем мы докажем завершаемость программы на φ (метод фундированных множеств Флойда). Из этого, по лемме 1, будет следовать полная корректность.

Введем две функции: функция пути и предикат пути. Пусть у нас есть блок схема Р и путь α, состоящий из связок е0,…, ek , k≥0.



n0,…,nk+1 – операторы блок-схемы.

Предикат пути:



Если его значение истинно, то вычисление блок схемы, в котором в начале вычисления пути выполняется этот предикат, пойдет строго по пути α, и мы нигде не свернем с этого пути.

Функция пути:



Эта функция определяет значения промежуточных переменных после прохождения по пути α, при условии, что в начале пути значения переменных соответствовали значениям параметров.

Дадим строгое индуктивное определение.

Базис индукции: если путь состоит из одной связки у0, то:



Пусть мы определили эти две функции для всех путей длины ≤k. Рассмотрим путь длины k+1:




Значение функций будет определяться в зависимости от оператора n1.

1)


2)



3)


Другие операторы не могут присутствовать на месте n1: у START нет входа, у HALT – выхода. Но мы доопределим:

4)


5)



Функция пути возвращает значение выходных переменных.
Построим эти функции для примера. Рассмотрим путь:



Метод индуктивных утверждений Флойда


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

Шаг 1. Точки сечения.

На первом шаге мы должны выбрать некоторое множество связок, чтобы выполнялось условие: любой цикл в блок-схеме должен разбиваться одной из связок выбранного множества. В нашем примере С={B}. Элементы множества С называются точками сечения.

Шаг 2. Индуктивные утверждения.

Для каждой токи сечения из множества С мы должны выбрать предикат Pi

,

который называется индуктивным утверждением соответствующей точки сечения. Этот предикат характеризует отношение между переменными блок-схемы при прохождении данной связки. Для примера:



Шаг 3. Условия верификации.

Базовые пути – все пути, начинающиеся в точке сечения и завершающиеся в точке сечения и других точек сечения в этом пути нет (это промежуточные базовые пути). В примере один такой путь:


К базовым путям мы также будем относить все пути, начинающиеся в точке сечения и заканчивающиеся в операторе HALT, других точек сечения на пути нет (конечные базовые пути). В примере: B → C. Также рассматриваем начальные базовые пути: начало в операторе START, конец в точке сечения, других точек сечения на пути также не должно быть. В примере: A → B. Бывает также вырожденный случай – начало пути в операторе START, конец в операторе HALT, и на этом пути нет точек сечения.


Для каждого вида пути определим условие верификации:



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

Метод фундированных множеств Флойда


Используем этот метод для доказательства завершимости программ на входном предикате. Фундированное множество – это частично упорядоченное множество, которое не содержит бесконечно убывающих последовательностей. Например, множество натуральных чисел.

Метод также состоит из трех шагов.

Шаг 1. Построение точек сечения. Аналогично предыдущему методу.

Шаг 2. Оценочные функции. Строим оценочную функцию для каждой точки сечения.



W – фундированное множество, единое для всех точек сечения.

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

Шаг 3. Условия завершимости. На этом шаге мы формулируем условия завершимости для каждого промежуточного базового пути нашей блок-схемы:



- отношение «больше» на множестве W.

Если мы докажем эти условия завершимости, то мы докажем завершимость блок-схемы относительно входного предиката. Таким образом, при помощи двух методов мы доказали полную корректность блок-схемы относительно предикатов φ и ψ.

Рассмотрим действие этих методов на примере. Ранее мы построили сечение, индуктивные утверждения, функции и предикаты пути. Запишем условия верификации для всех базовых путей.



Раскрыв скобки в правой части, мы получим, что утверждение истинно.



Эта формула тоже верна.



Утверждение также всегда выполнено.

Таким образом мы доказали частичную корректность.

Докажем теперь завершимость. Точки сечения и индуктивные утверждения остаются неизменными, поэтому не надо дополнительно ничего доказывать. Выберем оценочные функции и фундированное множество. Пусть W = Nat, UB(x1,x2,y1,y2) = y2. Мы выбрали такую функцию, потому что значение y2 все время уменьшается и ограничено нулем, поэтому когда-нибудь мы должны выйти из цикла. Формально, в индуктивном утверждении мы должны добавить требование (x2>0) и доказать для данного утверждения все условия верификации. Но т.к. переменная x2 не меняется и по предусловию x2>0, то в любой точке программы выполнено условие x2>0. Запишем условие завершимости для промежуточного базового пути:



Это утверждение также является истинным. Следовательно: <φ>P.

Таким образом, по лемме 1, выполнено <φ>P<ψ>, т.е. мы доказали полную корректность программы относительно пред и постусловий.