Файл: Технология раработки програмного обеспечения УП.pdf

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).

Остановимся

на

нескольких

важных

моментах

в

связи

с

доказательством

правильности

программ.

•

Доказательства

длинны

и

сложны

даже

для

простой

программы.

•

Если

оперировать

нецелочисленными

данными,

то

формулировка

аксиом

становится

затруднительной.

Операции

со

строками,

плавающей

точкой,

доступ

к

базам

данных

вызывают

серьезные

осложнения

при

аксиоматическом

подходе.