Учебное пособие: Технология раработки програмного обеспечения УП
81
граммы.
Эти
правила,
называемые
правилами
следствия,
фор-
мулируются
следующим
образом:
1)
если
{P}S{Q}
и
Q
⇒ R,
то
{P}S{R};
2)
если
{Q}S{R}
и
P
⇒ Q,
то
{P}S{R}.
Первое
правило
заключается
в
следующем:
«Если
P
—
предусловие
для
Q
и
если
Q
⇒ R
является
теоремой
исчисления
предикатов,
то
P
—
предусловие
для
R».
Таким
образом,
если
P
истинно
и
выполняется
S,
то
R
(так
же,
как
и
Q)
истинно.
Второе
правило
следствия
аналогично
данному.
Эти
пра-
вила
следствия
можно
представить
в
более
формальном
виде:
числитель
выражения
является
посылкой,
а
знаменатель
—
за-
ключением:
1)
{ } { }
{ } { }
;
,
P S Q
Q
R
P S R
⇒
2)
{ } { }
{ } { }
.
,
Q S R
P
Q
P S R
⇒
Правила
следствия
используются
для
доказательства
сложных
элементов
программы.
Пусть
программа
представлена
в
виде
структуры
(рис.
5.1),
где
S
i
— операторы,
а
P
i
— преди-
каты,
соответствующие
дугам.
Рис.
5.1
—
Структура
программы
Предположим,
что
доказаны
следующие
утверждения:
{P
1
}S
1
{P
1
'}
и
{P
2
}S
2
{P
2
'}
для
некоторых
предикатов
P
1
'
и
P
2
'.
Если
можно
доказать,
что
P
1
'
⇒ P
2
и
P
2
'
⇒ P
3
,
то,
используя
правила
следствия,
можно
доказать,
что
{P
1
}S
1
;S
2
{P
3
}
истинно.
Следует
определить,
какие
операторы
программы
явля-
ются
правильными.
Предполагается,
что
программа
состоит
только
из
последовательности
операторов
присвоения
и
опера-
торов
if
и
do
while
.
Начало
Конец
S
1
S
2
P
1
P
2
P
3
82
Так
как
только
оператор
присвоения
может
изменять
зна-
чение
переменных,
то
для
определения
правильности
оператора
присвоения
нужно
добавить
только
одну
аксиому,
она
называ-
ется
аксиомой
присвоения
и
формулируется
следующим
обра-
зом:
( )
(
)
{
}
( )
{ }
.
expr,
expr
expr
x
P x
P
x
P x
=
=
В
соответствии
с
этой
аксиомой
устанавливается,
что
ес-
ли
P
— утверждение,
содержащее
переменную
x,
истинно,
то
P
должно
быть
истинно
и
до
выполнения
оператора
присвоения,
если
x
изменяется
expr.
Например,
если
P(x)
является
предикатом
x > 0
и
x = x + 1
—
оператор
присвоения,
то
P(x + 1)
является
предикатом
x + 1 > 0
или
x > –1.
По
правилам
следствия,
если
можно
доказать,
что
Q
⇒
P(x + 1)
для
некоторого
предиката
Q,
то
справедливо
утвержде-
ние
{Q}x = x + 1{x > 0}
и
предикат
является
предусловием
для
P.
Осталось
определить
правильные
управляющие
структу-
ры.
Введем
следующие
аксиомы.
Аксиома
следования:
{ } { } { } { }
{ }
{ }
1
2
1
2
.
,
;
P S Q
Q S
R
P S S
R
Два
оператора
программы
могут
быть
объединены.
Если
после
выполнения
S
1
предикат
Q
остается
истинным
и
Q
есть
предусловие
для
оператора
S
2
,
то
P
является
предусловием
для
операторов
S
1
; S
2
.
Аксиома
цикла:
{
} { }
{ }
( )
{
}
.
&
;
;
&
P
B S P
P do while B and
B
P
¬
Утверждается,
что
если
истинность
P
не
изменяется
опе-
ратором
S
(т.е.
является
инвариантом),
то
P
инвариантно
отно-
сительно
цикла,
содержащего
S.
Кроме
того,
при
выходе
из
цикла
значение
выражения
B
ложно.
Аксиома
выбора:
83
а)
{
} { } {
} { }
{ }
{ }
1
1
2
;
&
,
&
2
;
P
B S Q
P
B S
Q
P if B then S else S
Q
¬
б)
{
}
{ }
{ }
1
1
.
&
,
&
P
B S P
B
Q
P if B then S Q
¬ ⇒
Эти
аксиомы
устанавливают
простые
соотношения
для
оператора
if
.
5.2
Правила
преобразования
данных
Коммутативность:
;
.
x
y
y
x
x
y
y
x
+ = +
× = ×
Ассоциативность:
(
)
(
)
(
)
(
)
;
.
x
y
z
x
y
z
x
y
z
x
y
z
+
+ = +
+
× × = × ×
Дистрибутивность:
(
) (
) (
)
.
x
y
z
x
y
x
z
×
+
=
×
+
×
Вычитание:
.
x
y
y
x
− + =
Обработка
констант:
0
;
0
0;
1
.
x
x
x
x
x
+ =
× =
× =
5.3
Доказательства
правильности
программ
Используя
приведенные
выше
правила
и
аксиомы,
можно
осуществлять
доказательство
правильности
программ.
Рассмот-
рим
следующую
программу:
1.
MULTIPLY (R,A,B);
2.
declare
X;
3.
declare
R; /* R=A*B */
4.
declare
A,B; /* B
≥0 */
5.
R=0;
84
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
—
выражение
внутри
цикла
ложно.
85
Таким
образом,
если
выражение
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).
Остановимся
на
нескольких
важных
моментах
в
связи
с
доказательством
правильности
программ.
•
Доказательства
длинны
и
сложны
даже
для
простой
программы.
•
Если
оперировать
нецелочисленными
данными,
то
формулировка
аксиом
становится
затруднительной.
Операции
со
строками,
плавающей
точкой,
доступ
к
базам
данных
вызывают
серьезные
осложнения
при
аксиоматическом
подходе.