Информатика и компьютерные науки (стр. 9 из 14)

{P^B}S1{Q},{P^~B}S2{Q}.

{Р} if В then S1 else S2 {Q}

Теперь рассмотрим два варианта условного оператора и обеспечим для каждого правила вывода. Первый вариант получается, когда мы замечаем, что в if B then S1 else S2 S2 может быть любым и, в частности, пустым оператором. Пустой оператор определяет тождественную операцию, т. е. операцию, не воздействующую на значения переменных. Если S2 — пустой оператор, то (2.38) запишется так:

if B then S. (2.41)

Действие, которое определяется этим оператором, вначале состоит в вычислении В. Если В истинно, то должно быть выполнено действие, определяемое S, иначе должна быть выполнена тождественная операция. Выражение (2.41) можно представить рис. 2Д.

Теперь определим соответствующее правило вывода. Если мы хотим доказать {P} if B then S{Q}, то необходимо обеспечить два условия. Первое из них заключается в том, что если S выполняется, то Q справедливо после его завершения. Так как при условии истинности В для выполнения выбирается S, то выводим, что Р /\В справедливо перед выполнением S, если Р справедливо перед выполнением (2.41). Итак, требуется доказать {p^b}s{q}. Второй случай имеет место, когда S не выполняется, т.е. когда после вычисления В получается значение ложь. Итак, в этой точке справедливо Р ^ ~В, и если Q справедливо после выполнения (2.41), то необходимо доказать, что Р ^ ~В ® Q. Альтернативой получения правила вывода является рассмотрение (2.41) в эквивалентной форме:

if B then S else. (2.42)

В (2.42) после else идет пустой оператор. Но в любом случае правило вывода формулируется следующим образом:

{P^B}S{Q},P^~B®Q .

{Р} if В them S {Q}

2.5. ОПЕРАТОРЫ ИТЕРАЦИИ

Теперь обратимся к структурам, которые приводят к циклам. Сначала изучим конструкцию while-do, а затем repeat-until.

Операторы while-do

Если В — Булево выражение и S — оператор, то

while В do S (2.47)

обозначает итерационное выполнение оператора S, пока В истинно. Если В ложно с самого начала, то S не будет выполняться совсем. Процесс итерационного выполнения S оканчивается, когда В становится ложным. Эта ситуация изображена на рис. 2Ж.

Задав любое начальное неотрицательное целое значение п, можно воспользоваться этим оператором для вычисления суммы I2 + 22 + ... +п2, получаемой как конечное значение h в следующей программе:

begin h := 0;

while n > 0 do begin h: = h + n *n; n: = п - 1 end

Теперь необходимо изучить утверждение {Р} while В do S {Q}, для чего рассмотрим рис. 2Ж более подробно, т. е. перейдем к рис. 23. Если Р справедливо, когда мы впервые входим в рис. 23, то ясно, что Р^В будет справедливо, если мы достигнем точки С Тогда если мы хотим быть уве-

ренными, что Р снова выполняется при возврате в точку А, нам необходимо обеспечить истинность для S утверждения {Р ^ В} S {Р}.

В этом случае ясно, что Р будет выполняться не только тогда, когда точка А на рис. 23 достигается первый или второй раз, но и после произвольного числа итераций. Аналогично Р ^ В выполняется всякий раз, когда достигается точка С. Когда достигается точка выхода D (см. рис. 23), то справедливо не только Р, но и ~В. Итак, получаем следующее правило вывода:

{p^b}s{p}

{Р} while В do S {Р ^ ~В}

Заметим, что (2.49) устанавливает свойство инвариантности Р для цикла в (2.49). Если Р выполняется для начального состояния вычисления, то оно будет выполняться для состояния вычисления, соответствующего каждому прохождению цикла. Р составляет сущность динамических процессов, которые происходят при выполнении (2.47). Далее будем называть Р инвариантом цикла.

Операторы repeat-until.

Другая форма оператора итерации:

repeat S until В, (2.50)

где S — последовательность операторов и В — Булево выражение. Оператор (2.50) определяет, что S выполняется перед вычислением B. Затем, если В ложно, процесс итерационного выполнения S продолжается, в противном случае он завершается. Структура оператора итерации (2.50) представлена на рис. 2И.

Сравнивая рис. 2Ж и 2И, замечаем, что на рис. 2И S должен быть выполнен по меньшей мере один раз, в то время как на рис. 2Ж он может не выполняться совсем.

Пример оператора repeat-until дан в программе (2.51), которая вычисляет сумму h=12+22+...+n2 для заранее заданного значения п:

begin h:=0;

repeat h: = h + n * п;

п := п — 1

until n= 0 (2.51) end

Предположим, что допускаются отрицательные значения п. Тогда можно использовать (2.48) и (2.51) для иллюстрации фундаментальной проблемы, связанной с итерационной композицией, когда мы заинтересованы в полной, а не в частичной корректности. Если n<=0, то (2.51) является бесконечным циклом. С другой стороны, программа (2.48) завершается, даже если n<=0. Таким образом, видим, что неправильно спроектированный оператор итерации может фактически описывать бесконечное вычисление.

Чтобы установить правило вывода для repeat S until В, рассмотрим рис. 2К. Предположим, доказано, что {Р} S {Q} и Q ^~B ® Р. Тогда если Р истинно в точке входа, то Q будет истинно, когда точка С достигается в первый раз.

Если В ложно, то истинно Q ^ ~В, и при прохождении через цикл вновь достигается точка А. Так как Q/&bsol;~В ®.Р, то, следовательно, Р удовлетворится при достижении точки А во второй раз (если это вообще происходит). Но тогда вновь на основании [Р] S {Q} будет удовлетворяться Q, когда точка С достигается во второй раз, и т.д. Итак, видно, что при сделанных предположениях Р будет истинно всякий раз, когда достигается точка А, и Q будет истинно всякий раз, когда достигается точка С, независимо от числа повторений цикла. Когда итерационный процесс заканчивается, т.е. когда достигается точка выхода D на рис. 2К, то должно быть истинно утверждение Q^B. Это рассуждение приводит к следующему правилу вывода:

{P}S{Q},Q^~B®P

{Р} repeat S until B{Q^B]

Покажем, как заменить оператор repeat-until структурной схемой, в которой цикл задается оператором while-do. Вспомним идею repeat S until В — выполнить S, а затем проверить В, затем выполнить снова S, если В ложно, и повторять этот процесс. Другими словами, выполнить S, повторяя затем выполнение S до тех пор, пока В не станет истинным. Таким образом, имеем эквивалентность:

repeat Suntil В = begin S; while ~Bdo S end. (2.53)

Теперь проверим, что (2.53) позволяет вывести правило для repeat-until (2.52) из правила вывода while-do

{P^B} S {P} (2.49)

{P}while B do S{P^~B}

и правила вывода

{P}S1{R},{R}S2{Q]

{Р} begin S1; S2 end {Q}' (2.54)

Нам потребуется также правило консеквенции

Р ® R, {R} S {Q}

{Р} S {Q}

Если задано {Р} S {Q}, то естественно берем Q в качестве соотношения в точке входа в while ~В do S (рис. 2Л), которое приводит к использованию (2.49) в модифицированном виде

{Q^~B}S[Q}

{Q} while ~В do S {Q ^ В}

где применяется равенство ~~B =В. Теперь, вместе с соответствующей заменой переменных, из правила консеквенции (2.55) вытекает:

Q^~B®P,{P}S[Q}

{Q^~B}S{Q]

комбинация которого с (2.56) дает

{P}S{Q},Q^~B®P

{Q} while ~В do S {Q ^ В}

Затем, используя (2.54), получаем искомый результат

[p}s{q},q^ ~b®p

{Р} begin S; while ~В do S end {Q ^ B}

который с учетом заданной эквивалентности (2.53) и есть то, что требовалось доказать.

2.7. ИСПОЛЬЗОВАНИЕ ОСНОВНЫХ ПРАВИЛ ВЫВОДА

Алгоритм деления.

В качестве примера доказательства корректности программы применим полученные нами правила вывода для доказательства корректности программы деления неотрицательных целых чисел (см. рис. 2.1). Пусть читатель теперь проверит, что структурная схема действительно отображена в следующей программе на языке Паскаль. Заметим, что соотношения (комментарии, заключенные в { }) не являются частью собственно программы, а описывают существенные аспекты состояния вычислений в соответствующих точках, определенных в процессе проектирования сверху вниз:

{(х>=0)^(y>0)} begin q:= 0;

r := х;

{(x=q*y+r)^(0<=r)}

while r > у do

{(x=q*y+r)n(0<y<=r)}

begin r : = r — у;

q:=1+q

end end {(x=q*y+r)^(0<=r<y)} (2,58)

Критерий корректности (2.58) выражается соотношением (х= q *у + r) ^ (0 <= r <у), которое должно иметь место при завершении (2.58),

если (х>=0) ^ (у>0) справедливо перед выполнением (2.58). Это мы и должны доказать.

Рассмотрим сначала цикл в нашей программе, представленный Sз на рис. 2.2 в (рис. 2М). В этом примере В имеет вид (r>= у). Если теперь заметить, что выходное соотношение на рис. 2.2в может быть переписано как

(х=q*у+r)^(r>=0)^~(r>=у), то ясно, что это как раз и есть Р ^ ~В, где P — это

(x=q*y+r)^(r>=O). (2.59)

Другими словами, наша задача при верификации рис. 2М — показать, что

{P} while (r >= у) do S2 {Р ^ ~(г >= у)}, где инвариант цикла Р задается (2.59). Но правило вывода

{P^B}S{P}

{Р} while В do S {Р ^ ~В}

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

{P^(r>=y)}S2{P} (2.61) для Р,

задаваемого (2.59), и S2, задаваемого

begin r := r —у; q := 1 + q end,

которое является только версией на языке Паскаль на рис. 2.26. Теперь (x=q*y+r)^(r>=0)^(r>=y®(x=(1+q)*y+(r-y))^(r-y>=0). Вспоминая правило вывода для оператора присваивания, получим:

{(x=(l+q)*y+(r-y))^((r-y)>=0)}r:=r-y{(x=(l+q)*y+r)^(r>=0)},

{(х = (1 + q) * у + r) ^ (г >= 0)} q : = 1 + q {(х = q * у + r) ^ (r >= 0)}.

Из правила вывода для составного оператора и правила консеквенции следует:

{(x=q*y+r)^(r>=0)^(r>=y)} begin r := r — y',q := 1 + q end

{(x=q*y+r)^(r>=0)}, (2.62)

которое есть в точности выражение (2.61), необходимое для доказательства. Таким образом, правило вывода (2.60) позволяет вывести требуемое условие

{(х = q * у + r)^{r >= 0)} S3 {(x= q *у + г)^(r >= 0)^ ~(г >=у)}. (2.63)

Следующий шаг состоит в проверке того, что требуемое условие

{(х >= 0) ^ (у > 0)} begin q : = 0; r : = х end {(х = q * у + r) ^ (r >= 0)} (2.64)

выполняется для S1 на рис. 2.2. Действительно,

(х >= 0) ^ (у > 0) ® {х = 0 * у + х) ^ (х >= 0)

{(х = 0 * у + х) ^(х >= 0)} q := 0 {(х = q * у + х)^(х >= 0)}

{(x=q*y+x)^(x>=0)} r:=x {(x=q*y+r)^(r>=0)}. (2.65)

Из (2.65), используя правило консеквенции и правило для составного оператора, выводим, что (2.64) выполняется.

Теперь из (2.63), (2.64) и правила вывода для составного оператора следует:

{(х>=0)^(у>0)} begin q := 0; r := х;

while r >= у do

begin r := r — у, q := 1 + q end end {(x=q*y+r)^(0<=r<y)],