Дудаков С.М. Математическое введение в информатику

Подождите немного. Документ загружается.

4.4. Построение структурированных программ 101

потому что ρ

w = 1, но, в то же время,

6|= y = α

потому что

y = σ

y = λ

= α

6= α

а в программе с метками нет двух одинаковых меток операторов.

Из определения семантики для неполного ветвления получаем, что

ϕ (o

)





= ρ

Рассмотрим ϕ (o

)





при k = j

. Тогда

|= w = succ (0)

|= y = α

так как

y = σ

y = λ

= α

Пусть π

= ϕ (o

)





 1. Если

∼ α

= e

; β

то по определению семантики присваивания и следования и по опреде-

лению семантики программы с метками получим, что

y = β

= λ

i+1

w = 0,

= ρ

) = σ

i+1

) .

Для всех остальных переменных z будем иметь

z = ρ

z = σ

i+1

 2. Пусть теперь

∼ α

if T

then β

else γ

Тогда

 Var





= ρ

 Var





= σ

 Var





= σ

 Var





= σ

i+1

 Var





102 Глава 4. Программы с метками

Кроме того, π

w = 0 и

y =



, если ρ

|= T

, если ρ

6|= T





, если σ

|= T

, если σ

6|= T



= λ

i+1

Теперь рассмотрим ϕ (o

)





при k > j

. Очевидно, что

6|= w = succ (0) ,

поскольку π

w = 0. Значит, ϕ (o

)





= π

Итак, мы доказали, что σ

i+1

= Π





= π

. Но при рассмотрении

случая k = j

мы показали, что π

удовлетворяет условиям утверждения.

Следовательно, утверждение доказано для i+1 и, по индукции, для всех

i, для которых метка λ

i−1

не заключительная.

Пусть Π

(σ) определено. Тогда последовательность расширенных со-

стояний



, λ



конечна. Предположим, что (σ

, λ

) — ее последний

элемент. Тогда λ

должна быть заключительной меткой. То есть, λ

6= α

для k = 1, . . . , m. Это означает, что ϕ (o

)





= ρ

для k = 1, . . . , m.

Но тогда σ

n+1

= ρ

n+1

6|= w = 0,

так как ρ

w = 1. Это означает, что Π

(σ) = σ

n+1

. Но

n+1

 Var





= σ

 Var





= σ

 Var





Пусть теперь Π

(σ) определено. Тогда последовательность





ко-

нечна. Пусть σ

— последний элемент. Это означает, что

6|= w = 0.

Так как σ

= Π



n−1



, то Π



n−1



(w) 6= 0. Если бы для некоторого

k = 1, . . . , m имело бы место σ

n−1

y = α

, то Π



n−1



(w) = 0. Значит,

6= σ

n−1

y для всякого k = 1, . . . , m. Согласно утверждению, σ

n−1

y =

n−1

. Это означает, что метка λ

n−1

является заключительной и Π

(σ) =

n−1

. Далее, очевидно, что

n−1

 Var





= σ

 Var





Следовательно,

(σ)  Var





= σ

n−1

 Var





4.4. Построение структурированных программ 103

= σ

n−1

 Var





= σ

 Var





= Π

(σ)  Var





Задача 4.10. Структуризируйте программы Min с рис. 4.1 на стр.

84 и F ib с рис. 4.2 на стр. 87 методом, пр едложенным в теореме.

∗

Задача 4.11. Модифицируйте доказательство теоремы так, что ес-

ли исходная программа с метками является простой, то построенная

структурная программа тоже будет простой.

Итак, мы доказали, что структурированные программы и программы

с метками вычисляют одни и те же функции. Выведем следствие.

Следствие 4.5. (Теорема о цикле) Для всякой структурной про-

граммы Π существует структурная программа Π

, которая содержит

только один оператор цикла и

Π (σ)  Var (Π) = Π

(σ)  Var (Π)

для любого состояния σ программы Π

Доказательство. Для Π существует программа с метками Π

такая,

что

Π (σ) = Π

(σ)

для любого состояния σ. По теореме о структуризации существует струк-

турная программа Π

, которая содержит один оператор цикла и

(σ)  Var (Π) = Π

(σ)  Var (Π)

для любого состояния σ программы Π

. Следовательно,

Π (σ)  Var (Π) = Π

(σ)  Var (Π)

для любого состояния σ.

∗

Задача 4.12. Сформулируйте теорему о подстановке для программ

с метками и, используя теоремы о построении программ с метками и

о структуризации, докажите ее.

∗

Задача 4.13. Сформулируйте и докажите теорему о простой про-

грамме для программ с метками.

Глава 5

Доказательство корректности

структурированных программ

Мы уже несколько раз доказывали, что написанные нами программы

действительно работают корректно, то есть делают именно то, для чего

мы их писали. Эти доказательства были достаточно сложными и заклю-

чались в рассмотрении различных состояний.

Имеется другой путь — сформулировать некоторые формальные пра-

вила следуя которым можно из истинных утверждений о программах

получать истинные, и, пользуясь этим, доказывать корректность.

5.1 Исчисления

Определение 5.1. (Исчисление) Исчисление I — это тройка

(S, A, R). S — множество синтаксических конструкций, A ⊆ S —

множество аксиом, R — множество правил вывода. Правило вывода

r — частичное отображение

r : S

<ω

→ P (S) .

То есть по каждой конечной последовательности s

, . . . , s

, s

∈ S пра-

вило вывода дает множество S

⊆ S.

Определение 5.2. (Доказательство, вывод) Доказательство (вы-

вод) в исчислении I = (S, A, R) — это конечная последовательность

, . . . , s

, где s

∈ S — синтаксические конструкции, и для каждого

i = 1, . . . , n или s

∈ A (то есть s

— аксиома), или существует прави-

ло вывода r ∈ R такое, что s

∈ r (s

, . . . , s

i−1

) (то есть s

получено из

предыдущих элементов с помощью одного из правил вывода). Каждый

вывод является выводом своей последней синтаксической конструкции.

5.1. Исчисления 105

Определение 5.3. (Доказуемость, выводимость) Доказуемость в

исчислении I конструкции s (обозначается B

s) означает возмож-

ность построения в I вывода, последним элементом которого явля-

ется s. Обозначение

, . . . , A

означает доказуемость s в исчислении I

, полученном из I добавлением

аксиом A

, . . . , A

Определение 5.4. (Условие) Условие для программы Π — некоторое

свойство, сформулированное с использованием переменных программы

Π.

Пример 5.1. Пусть x, y и z — переменные. Примеры условий:

x < x

+ y

; x < y и y < z − x

;

существует v такое, что x < v < y и v делится на z

Мы будем использовать для записи условий язык математической ло-

гики и записывать условия в виде формул логики предикатов:

x < x

+ y

; x < y ∧ y < z − x

; ∃v



x < v < y ∧ z



Определение 5.5. (Истинность условия) Условие ϕ истинно на со-

стоянии σ: σ |= ϕ, если при подстановке в ϕ вместо переменных x

их значений на σ, то есть σx, то получается формула, которая ис-

тинна на предметной области. Истинность условия ϕ на состоянии

σ записываем в виде σ |= ϕ.

Ложность условия ϕ на состоянии σ (σ 6|= ϕ) означает отсут-

ствие истинности.

Замечание 5.1. Мы отличаем истинность на состоянии от истин-

ности на предметной области. Истинность на предметной области

означает истинность на любом состоянии (то есть по свободным пе-

ременным неявно навешиваются кванторы всеобщности).

Условие может содержать нелогические символы, которые явля-

ются общеизвестными (например, сложение или умножение нату-

ральных чисел). Таким образом, речь идет о предметной области не

просто как о множестве, а как об алгебраической системе, то есть о

множестве с определенными на нем отношениями и операциями.

106 Глава 5. Доказательство корректности структурированных программ

Пример 5.2. Пусть σ = {(x, 20) , (y, 25) , (z, 4)}. Тогда

1. σ |= x < y + z

, так как 20 < 25 + 4

2. σ |= x < y ∧ y < z + x

, так как 20 < 25 и 25 < 4 + 20

3. σ 6|= ∃u



x < u < y ∧ z



, потому что никакое число между 20 и

25 не делится на 16.

Задача 5.1. Определите, истинны ли три условия из предыдущего

примера на состояниях из примера 3.8 на стр. 42.

Определение 5.6. (Тройка Хоара) Тройка Хоара — формула вида

{ϕ}Π {ψ}, где Π — программа, а ϕ и ψ — условия для Π.

В тройке {ϕ}Π {ψ} предусловие — это формула ϕ, а постусло-

вие — ψ.

Для длинных троек мы будем писать предусловие, программу и по-

стусловие в столбик, ограничивая его прямыми линиями:



{ϕ}

{ψ}



Рассмотрим пример.

Пример 5.3. Возьмем следующую пр ограмму:

Π ∼ z = x; x = y; y = z;

Тройки Хоара для данной программы:



x < y + z



Π {x < y};

{x < y}Π



∃u



x < u < y ∧ z



;



∃u



x < u < y ∧ z





x < y + z



Определение 5.7. (Частичная корректность) Тройка Хоара

{ϕ}Π {ψ}

называется частично корректной на множестве состояний S, если

для всякого состояния σ ∈ S такого, что σ |= ϕ и Π (σ) определено,

выполнено Π (σ) |= ψ. Тройка называется частично корректной, если

она частично корректна на множестве всех состояний.

5.1. Исчисления 107

Определение 5.8. (Полная корректность) Тройка Хоара

{ϕ}Π {ψ}

называется полностью корректной (вполне коррекной) на множестве

состояний S, если для любого состояния σ ∈ S из σ |= ϕ следует, что

Π (σ) определено и Π (σ) |= ψ. Тройка называется полностью коррект-

ной, если она полностью корректна на множестве всех состояний.

Интуитивно это означает следующее. Предусловие — свойство, кото-

рому должны удовлетворять входные данные программы. Постусловие

описывает результат работы программы. Частичная корректность: ес-

ли программа останавливается для допустимых входных данных, то ре-

зультат верен. Полная корректность: если входные данные допустимы,

то программа останавливается и результат верен.

Следствие 5.1. Если тройка Хоара полностью корректна, то она ча-

стично корректна.

Следствие 5.2. Каждая тройка полностью корректна на пустом

множестве.

Задача 5.2. Докажите оба следствия.

Пример 5.4. Рассмотрим следующую программу:

while x < y do

x = succ (x) ;

y = succ (y) ;

if y = 5 then

y = 0;

end;

Семантика этой программы такова:

если σ 6|= x < y, то Π (σ) = σ;

если σ |= x < y и σy < 5, то

Π (σ) = {(y, 0) ; (x, σx − σy + 5)};

если σ |= x < y и σy ≥ 5, то Π (σ) не определено.

108 Глава 5. Доказательство корректности структурированных программ

Пусть

ϕ ∼ x = y ∧ y < 3, ψ ∼ y

< 5.

Если σ |= ϕ, то σ 6|= x < y, следовательно, Π (σ) = σ. Это означает,

что тройка {ϕ}Π {ψ} полностью корректна, так как если σ |= ϕ, то

Π (σ) определено и Π (σ) |= ψ.

Пусть

ϕ ∼ y − x = 4, ψ ∼ x + y = 1.

Тогда σ |= x < y. Если σy < 5, то σy ≤ 4. Это значит, что σy = 4 и

σx = 0, следовательно, Π (σ) определено и

Π (σ) = {(y, 0) ; (x, 1)}.

Для остальных σ таких, что σ |= ϕ, Π (σ) не определено. Итак, тройка

{ϕ}Π {ψ} является частично корректной, но не является полностью

корректной.

Пусть

ϕ ∼ x + y = 5, ψ ∼ x − y = 3.

Рассмотрим следующее состояние: σ = {(x, 2) , (y, 3)}. Очевидно, σ |=

ϕ. Далее, σ |= x < y и σy < 5. Следовательно, Π (σ) определено и

Π (σ) = {(y, 0) ; (x, 4)}.

Ясно, что Π (σ) 6|= ψ. Таким образом, тройка {ϕ}Π {ψ} не является

частично корректной (и, тем более, полностью корректной).

Задача 5.3. Для каждой из программ из примера 3.5 на стр. 35 напи-

шите по три тройки Хоара, одна из которых должна быть полность

корректной, другая частично корректной, но не полностью коррект-

ной, третья — не частично корректной. Для всех ли программ это

можно сделать?

Замечание 5.2. Если Π (σ) определено для любого σ, то для любой

тройки Хоара с программой Π полная и частичная корректности эк-

вивалентны.

Замечание 5.3. Чтобы установить, что алгоритм

Alg A;

arg x

, . . . , x

;

end;

5.2.

∗

Исчисление Хоара 109

вычисляет (частичную) функцию Φ

достаточно доказать, что

тройка

= v

∧ ··· ∧ x

= v

∧ v ∈ dom Φ

}Π

{A = Φ

(v)}

полностью корректна. Предполагается, что переменные v не встреча-

ются в Π

Задача 5.4. Почему в предыдущем замечании необходимо, чтобы пе-

ременные v не встречались в Π

? Приведите пример, который доказы-

вает существенность этого условия.

5.2

∗

Исчисление Хоара

Мы определим исчисление Хоара — IH

. Синтаксическими конструк-

циями будут тройки Хоара. Доказуемость тройки Хоара в этом исчисле-

нии будет означать полную и/или частичную корректность этой тройки.

У нас будут аксиомы вида:

АКС {(ϕ)

}x = e; {ϕ}, где x — переменная, e — выражение.

Правила вывода исчисления IH:

УПР Усиление предусловия: если выводимо {ϕ}Π {ψ} и формула

θ → ϕ истинна на предметной области, то выводимо {θ}Π {ψ}.

ОП Ослабление постусловия: если выводимо {ϕ}Π {ψ} и формула

ψ → θ истинна на предметной области, то выводимо {ϕ}Π {θ}.

СЛ Правило следования: если выводимы тройки {ϕ}Π

{θ} и

{θ}Π

{ψ}, то выводимо {ϕ}Π

{ψ}.

НВ Правило неполного ветвления: если выводимо {ϕ ∧ T }Π

{ψ} и

формула ϕ ∧¬T → ψ истинна на предметной области, то выводимо

{ϕ} if T then Π

end; {ψ}.

ПВ Правило полного ветвления: если выводимы тройки

{ϕ ∧ T }Π

{ψ} и {ϕ ∧ ¬T }Π

{ψ}, то выводимо

{ϕ} if T then Π

else Π

end; {ψ}.

На самом деле мы определим два исчисления — одно для доказательства частичной коррект-

ности, др угое — полной. Эти исчисления будут отличаться только правилом, которое используется

для доказательства корректности цикла.

110 Глава 5. Доказательство корректности структурированных программ

Докажем, что с помощью аксиом можно доказать только вполне кор-

ректные тройки Хоара, а с помощью правил УПР–ПВ из корректных

троек получать корректные. Говоря языком математической логики, до-

кажем непротиворечивость исчисления Хоара.

 АКС Пусть Π ∼ x = e; пусть σ |= (ϕ)

, то есть ϕ истинно, если

вместо x подставить σ (e). Значит, если τ совпадает с σ во всем кроме

того, что τx = σ (e), то τ |= ϕ. Но по определению семантики оператора

присваивания, Π (σ) определено и Π (σ) = τ. То есть, Π (σ) |= ϕ. Это

означает полную корректность тройки {(ϕ)

}Π {ϕ}.

 УПР Пусть тройка {ϕ}Π {ψ} корректна и формула θ → ϕ истинна

на предметной области. Пусть σ |= θ. Из истинности θ → ϕ следует,

что σ |= ϕ.

1. Частичная корректность. Пусть Π (σ) определено. Тогда Π (σ) |=

ψ из-за частичной корректности {ϕ}Π {ψ}. Следовательно, тройка

{θ}Π {ψ} частично корректна.

2. Полная корректность. Так как σ |= ϕ и тройка {ϕ}Π {ψ} вполне

корректна, то Π (σ) определено и Π (σ) |= ψ. То есть тройка

{θ}Π {ψ} вполне корректна.

 ОП Пусть тройка {ϕ}Π {ψ} корректна и формула ψ → θ истинна на

предметной области. Пусть σ |= ϕ.

1. Частичная корректность. Пусть Π (σ) определено. Тогда Π (σ) |= ψ

из-за частичной корректности {ϕ}Π {ψ}. Из истинности ψ → θ по-

лучаем Π (σ) |= θ. Следовательно, тройка {ϕ}Π {θ} частично кор-

ректна.

2. Полная корректность. Так как σ |= ϕ и тройка {ϕ}Π {ψ} вполне

корректна, то Π (σ) определено и Π (σ) |= ψ. Из истинности ψ → θ

получаем Π (σ) |= θ. То есть тройка {ϕ}Π {θ} вполне корректна.

 СЛ Пусть тройки {ϕ}Π

{θ} и {θ}Π

{ψ} корректны. Пусть σ |= ϕ.

1. Частичная корректность. Пусть (Π

) (σ) = Π

(Π

(σ)) опреде-

лено. Тогда Π

(σ) определено и Π

(Π

(σ)) определено. И з ча-

стичной корректности {ϕ}Π

{θ} следует, что Π

(σ) |= θ. Из ча-

стичной корректности {θ}Π

{ψ} следует Π

(Π

(σ)) |= ψ. То есть

(Π

) (σ) |= ψ и тройка {ϕ}Π

{ψ} частично корректна.