Общие положения
Традиционные методы анализа ПО включают, в том числе, методы доказательства правильности программ. Начало этому направлению было положено работами П.Наура и Р. Флойда, в которых сформулирована идея приписывания точке программы так называемого индуктивного, или промежуточного утверждения и указана возможность доказательства частичной правильности программы (то есть соответствия друг другу ее предусловия и постусловия), построенного на установлении согласованности индуктивных утверждений.
| 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 ddi=d
i>0 ddi=2*ddi-1.
Далее с помощью обычных математических приемов можно вывести, что:
ddn=d*2n (2.1)
Кроме того, поскольку d>0, можно сделать вывод, что для любого конечного значения r отношение ddk>r будет выполняться при некотором конечном значении k; первый цикл завершается при dd=d*2k. Решая уравнение di=2*di-1
относительно di-1, получаем di-1=di/2, что позволяет утверждать, что второй цикл тоже завершится. По окончании первого цикла dd=ddk и поэтому выполняется соотношение
0£r<dd (2.2)
Это соотношение сохраняется при выполнении повторяемого оператора второго заголовка. После завершения повторений (в соответствии с заголовком while dd¹d do) мы получаем dd=d. Отсюда и из соотношения 2.2 следует, что
0£r<d (2.3)
Далее мы доказываем, что после начала работы программы всегда выполняется отношение:
ddº0(mod d) (2.4)
Это следует, например, из того, что возможные значения dd имеют вид (см. 2.1) d*2i при 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.
Как мы можем видеть, что программа, состоящая всего из нескольких строчек кода, может требовать формального доказательства ее правильности (т.е. доказательства соответствия предусловия и постусловия, а также доказательства завершимости), состоящего из нескольких страниц текста.
Таким образом, чтобы доказать правильность программы, сегмента программы или оператора, формулируется математическая теорема о результатах выполнения рассматриваемого сегмента программы. Затем эта теорема доказывается.
Почти всегда подобные теоремы формулируются следующим образом [Бей]. «Если конкретное условие истинно непосредственно перед выполнением сегмента программы, тогда после выполнения этого сегмента тоже истинным будет некоторое условие (в общем случае другое)».
Как было сказано выше, такие условия принято называть предусловиями и постусловиями. Предусловия и постусловия основаны на переменных из программы. На самом деле в большинстве условий используются лишь значения переменных в программе. В данном случае мы будем рассматривать лишь предусловия и постусловия именно такого вида.
Для упрощения доказательства теорема о корректности в приведенной выше форме разбивается на две части. Одна часть служит для доказательства того, что рассматриваемый сегмент программы вообще работает, то есть его выполнение заканчивается получением некоторого определенного результата (без ошибок на фазе компиляции или выполнения).В другой части доказывается корректность упомянутой теоремы в предположении, что программа завершает свою работу.
