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

   1. Общие положения

Традиционные методы анализа ПО включают, в том числе, методы доказательства правильности программ. Начало этому направлению было положено работами П. Наура и Р. Флойда, в которых сформулирована идея приписывания точке программы так называемого индуктивного, или промежуточного утверждения и указана возможность доказательства частичной правильности программы (то есть соответствия друг другу ее предусловия и постусловия), построенного на установлении согласованности индуктивных утверждений.

www.kiev-security.org.ua

BEST rus DOC FOR FULL SECURITY

Фундаментальный вклад в теорию верификации внес Ч. Хоор, высказавший идеи проведения доказательства частичной правильности программы в виде вывода в некоторой логической системе, а Э. Дейкстра ввел понятие слабейшего предусловия, позволяющее одновременно как соответствие друг другу предусловия и постусловия, так и завершимость. Методы доказательства правильности программ принесли определенную пользу программированию. Было отмечено, что эти методы указывают способ рассуждения о ходе выполнения программ, дают удобную систему комментирования программ и устанавливают взаимосвязи между конструкциями языков программирования и их семантикой. Если принять более широкое толкование термина «анализ программ», подразумевая доказательство разнообразных свойств программ или доказательство теорем о программах, то ценность методов анализа станет более ясной. В частности можно исследовать характер изменения выходных значений программы, количество операций при выполнении программы, наличие зацикливаний, незадействованных участков программы. Таким образом, в некоторых частных случаях методы верификации могут применяться и для доказуемого обнаружения программных дефектов.

Формальное доказательство в виде вывода в некоторой логической системе вполне надежно, но сами доказательства оказываются очень длинными и часто необозримыми. Рассмотрим следующий фрагмент программы [ДДХ].

integer r, dd;

r:=a; dd:=d;

while ddr do dd:=2*dd;

while ddd do

begin dd:=dd/2;

if ddr do r:=r-dd;

end.

Должно соблюдаться условие, что целые константы aиdудовлетворяют отношениямadиd>0.

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

i=0 dd_i=d

i>0 dd_i=2*dd_i-1.

Далее с помощью обычных математических приемов можно вывести, что:

dd_n=d*2ⁿ (2.1)

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

0r<dd(2.2)

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

0r<d(2.3)

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

dd0(mod d) (2.4)

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

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

ar(mod d) (2.5)

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

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

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

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

Как мы можем видеть, что программа, состоящая всего из нескольких строчек кода, может требовать формального доказательства ее правильности (т.е. доказательства соответствия предусловия и постусловия, а также доказательства завершимости), состоящего из нескольких страниц текста.

Таким образом, чтобы доказать правильность программы, сегмента программы или оператора, формулируется математическая теорема о результатах выполнения рассматриваемого сегмента программы. Затем эта теорема доказывается.

Почти всегда подобные теоремы формулируются следующим образом [Бей]. «Если конкретное условие истинно непосредственно перед выполнением сегмента программы, тогда после выполнения этого сегмента тоже истинным будет некоторое условие (в общем случае другое)».

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

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