Используя приведенные выше правила и аксиомы, можно осуществлять доказательство правильности программ. Рассмотрим следующую программу:
1. MULTIPLY (R,A,B);
2. declare X;
3. declare R; /* R=A*B */
4. declare A,B; /* B³0 */
5. R=0;
6. X=B;
7. do while (X¹0);
8. R=R+A;
9. X=X-1;
10. end;
11. end MULTIPLY;
Входным утверждением является предикат B ≥ 0, выходное утверждение R = A×B.
Общая схема доказательства правильности программы:
Строка 5.
· {0 = 0 & B ≥ 0} R = 0 {R = 0 & B ≥ 0} по аксиоме присваивания;
· {B ≥ 0} R = 0 {R = 0 & B ≥ 0} по правилу следствия в связи с тем, что истинны следующие утверждения:
истинно Þ 0 = 0;
B ≥ 0 Þ (B ≥ 0 & истинно).
Строка 6.
· {B = B & R = 0 & B ≥ 0} X = B {X = B & R = 0 & B ≥ 0} по аксиоме присвоения;
· {R = 0 & B ≥ 0} X = B {X = B & R = 0 & B ≥ 0} по аксиоме следования;
· {B ≥ 0} R = 0; X = B {X = B & R = 0 & B ≥ 0} по аксиоме следования.
Таким образом, показано, что если B ≥ 0 (входное предусловие), то после выполнения строки 6 выражение {X = B & R = = 0 & B ≥ 0} истинно.
Строки 7–10.
Необходим инвариант для предиката P цикла do while. Этот инвариант должен описывать работу, выполняемую циклом. В нашем случае цикл вычисляет произведение; таким образом, инвариантом может быть R = A×(B – X). В соответствии с аксиомой цикла, если можно показать, что это выражение инвариантно относительно цикла и что оно истинно, когда цикл заканчивается, то возникает следующая ситуация:
· R = A×(B – X) — инвариант цикла;
· X = 0 — выражение внутри цикла ложно.
Таким образом, если выражение R = A×(B – X) & (X = 0) истинно, то истинно и выражение R = A×(B – 0) & (X = 0), а это приводит к истинности соотношения R = A×B, что и требовалось доказать. Следовательно, для того, чтобы завершить доказательство, нужно, чтобы выражение R = A×(B – X) в строке 7 было истинно и оно является инвариантом цикла.
Доказательство того, что указанное выражение есть инвариант цикла, проводится следующим образом:
Строка 8.
· {R + A = A×B – A×X + A} R = R + A {R = A×B – A×X + A} по аксиоме присвоения;
· {R = A×B – A×X} R = R + A {R = A×B – A×X + A} по правилам целочисленной арифметики;
· {R = A×(B – X)} R = R + A {R = A×B – A×X + A} по правилам дистрибутивности.
Строка 9.
· {R = A×(B – (X – 1))} X = X – 1 {R = A×(B – X)} по аксиоме присвоения;
· {R = A×B – A×(X – 1)} X = X – 1 {R = A×(B – X)} по правилам целочисленной арифметики.
Объединение строк 8 и 9 в соответствии с аксиомой следования дает выражение {R = A×(B – X)} R = R + A; X = X – 1 {R= = A×(B – X)}, которое является желаемым инвариантом соотношения.
Теперь следует показать, что инвариантное выражение в строке 7 истинно, а это эквивалентно доказательству с помощью правил следования следующей теоремы: X = B & R = 0 & B ≥ 0 истинно в строке 6 Þ R = A×(B – X).
Остановимся на нескольких важных моментах в связи с доказательством правильности программ.
· Доказательства длинны и сложны даже для простой программы.
· Если оперировать нецелочисленными данными, то формулировка аксиом становится затруднительной. Операции со строками, плавающей точкой, доступ к базам данных вызывают серьезные осложнения при аксиоматическом подходе.
· Даже для относительно простого случая — использования целочисленных данных — существуют трудности. Например, все ЭВМ используют слова фиксированной длины для записи целых чисел. Возможно переполнение разрядной сетки, и аксиомы должны учитывать эти условия.
· Реальные языки программирования имеют встроенные структуры, которые нелегко поддаются проверке на правильность.
Несмотря на отмеченные недостатки, доказательства правильности программ достаточно широко применяются. Способы проверки правильности программ можно использовать при проектировании реальных программ. Для разрабатываемой программы должны быть определены предусловия работы. Даже если условия не доказаны формально, а просто установлены, они оказывают неоценимую помощь в понимании структуры разрабатываемой программы.
Добавление предусловий тесно связано с элементарными программами. Кроме того, предусловия являются базой для разработки тестов программ. Все предусловия могут быть закодированы как операторы if и выполняться как часть теста.