Безопасность программного обеспечения компьютерных систем


Формальные методы доказательства правильности программ и их спецификаций - часть 2


Рассмотрим последовательность значений, заданную выражениями для:

i=0 ddi=d i>0 ddi=2*ddi-1.

Далее с помощью обычных математических приемов можно вывести, что: ddn=d*2n (2.1.1)

Кроме того, поскольку d>0, можно сделать вывод, что для любого конечного значения r отношение ddr>r будет выполняться при некотором конечном значении k; первый цикл завершается при dd=d*2k. Решая уравнение di=2*di-1 относительно di-1, получаем di-1=di/2, что позволяет утверждать, что второй цикл тоже завершится. По окончании первого цикла dd=ddk и поэтому выполняется соотношение

0 r < dd (2.1.2)

Это соотношение сохраняется при выполнении повторяемого оператора второго заголовка. После завершения повторений (в соответствии с заголовком while ddd do) мы получаем dd=d. Отсюда и из соотношения (2) следует, что

0 r < d (2.1.3)

Далее мы доказываем, что после начала работы программы всегда выполняется отношение:

dd0(mod d) (2.1.4)

Это следует, например, из того, что возможные значения dd имеют вид (см. (1)) d*2i при 0 i k.

Следующая задача состоит в том, чтобы показать, что после присваивания r начального значения всегда выполняется отношение

ar(mod d) (2.1.5)

Оно выполняется после начальных присваиваний.

Повторяемый оператор первого заголовка (dd:=2*dd) сохраняет отношение (2.1.5), и поэтому весь первый цикл сохраняет отношение (2.1.5).

Повторяемый оператор из второго цикла состоит из двух операторов. Первый (dd:=2*dd) сохраняет инвариантность (2.1.5); второй тоже сохраняет отношение (2.1.5), так как он либо не изменяет значение r, либо уменьшает r на текущее dd, а эта операция в силу (2.1.4) также сохраняет справедливость отношения (2.1.5). Таким образом, весь повторяемый оператор второго цикла сохраняет отношение (2.1.5).

Объединяя отношения (2.1.3) и (2.1.5), получаем, что окончательное значение r удовлетворяет условиям 0 r < d и ar(mod d), то есть r - наименьший неотрицательный остаток от деления a на d.

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




Начало  Назад  Вперед



Книжный магазин