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

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

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

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

integer r, dd;
	r:=a; dd:=d;
	while ddr do dd:=2*dd;
	while ddd do dd:=2*dd;
		begin dd:=dd/2;
			if ddr do r:=rdd;
			end.
			

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

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

i=0	ddi=d
i>0	ddi=2*ddi1.
Далее с помощью обычных математических приемов можно вывести, что:
ddn=d*2n				

Кроме того, поскольку d>0, можно сделать вывод, что для любого конечного значения r отношение ddr>r будет выполняться при некотором конечном значении k; первый цикл завершается при dd=d*2k. Решая уравнение di=2*di1 относительно di1, получаем di1=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 имеют вид ) 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.

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

Большинство известных алгоритмов электронной цифровой подписи в качестве основной алгоритмической операции используют дискретное возведение в степень. Стойкость соответствующих криптографических схем основывается (как правило, гипотетически) или на сложности извлечения корней в поле GF(n), n произведение двух больших простых чисел, или на трудности вычисления дискретных логарифмов в поле GF(p), p большое простое число. Чтобы противостоять известным на данный момент методам решения этих задач операнды должны иметь длину порядка 512 или 1024 битов. Понятно, что выполнение вычислений над операндами повышенной разрядности (еще будет употребляться термин "операнды многократной точности" по аналогии с операндами однократной и двукратной точности) требует высокого быстродействия рабочих алгоритмов криптографических схем.


Ведете ли вы блог?

Да
Нет
Планирую


Результаты опроса

Новостной блок