Ім'я файлу: науки.doc
Розширення: doc
Розмір: 508кб.
Дата: 15.12.2020
скачати
Пов'язані файли:
реферат Правила торгівлі на ринках.doc
Информатика.doc
ПК науки.doc
Zadacha_1_ (3).doc
Розширення: doc
Розмір: 508кб.
Дата: 15.12.2020
скачати
Пов'язані файли:
реферат Правила торгівлі на ринках.doc
Информатика.doc
ПК науки.doc
Zadacha_1_ (3).doc
Правила (2.27) и (2.30) называются правилами консеквенции.
Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор — тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода
{Р}{Р}. (2.32)
Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р
{PXe}x:=e{P}. (2.33)
Здесь утверждается, что если Р истинно для подстановки е вместо х перед выполнением присваивания, то Р должно быть истинным, когда переменной х присвоили ее новое значение. Это правило лучше пояснить примерами, данными на рис. 2Б.
2.4. СОСТАВНЫЕ И УСЛОВНЫЕ ОПЕРАТОРЫ
Предположим, мы хотим доказать, что имеет место {Р} S {Q}, когда S является структурным оператором. Нам необходимо правило для каждого типа композиции операторов, которое позволит вывести свойства сложного (структурного) оператора на основе установленных свойств его компонент. В этом разделе обсуждаются такие правила для составных и условных операторов.
Составные операторы.
Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состо-
ящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)
и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).
Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:
{Р} S, [R], {R} S, {Q}
{Р}begin Si;S, end {Q} (2-36)
Правило вывода (2.36) обобщается следующим очевидным образом:
{Рi-1}S1{Pi} дпя i=1,....n
{P0} begin S1;. ..Sn. end {Pn}
Условные операторы.
Если S1 и S2 - операторы, а В — Булево выражение (т.е. выражение, имеющее значение Булевого типа), то
if В then S1 else S2 (2.38)
есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае — действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).
Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность [Р] if В then S1 else S2 {Q},то необходимо доказать два утверждения.
1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.
2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^
В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^
b}s2{q].
Если мы доказали как [Р^В] S1 {Q}, так и{Р^
В} S2 {Q}, то можно утверждать, что если Р справедливо перед выполнением (2.38), то Q будет справедливо по окончании его выполнения независимо от того, какой оператор (S1 или S2) был выбран для выполнения. Итак, можно сформулировать следующее правило вывода:
{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^
BQ .
{Р} 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/\
В .Р, то, следовательно, Р удовлетворится при достижении точки А во второй раз (если это вообще происходит). Но тогда вновь на основании [Р] S {Q} будет удовлетворяться Q, когда точка С достигается во второй раз, и т.д. Итак, видно, что при сделанных предположениях Р будет истинно всякий раз, когда достигается точка А, и Q будет истинно всякий раз, когда достигается точка С, независимо от числа повторений цикла. Когда итерационный процесс заканчивается, т.е. когда достигается точка выхода D на рис. 2К, то должно быть истинно утверждение Q^B. Это рассуждение приводит к следующему правилу вывода:
{P}S{Q},Q^
BP
{Р} 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^
BP,{P}S[Q}
{Q^
B}S{Q]
комбинация которого с (2.56) дает
{P}S{Q},Q^
BP
{Q} while
В do S {Q ^ В}
Затем, используя (2.54), получаем искомый результат
[p}s{q},q^
bp
{Р} 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
begin r : = r — у;
q:=1+q
end end {(x=q*y+r)^(0<=r
Критерий корректности (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)
Правила (2.27) и (2.30) называются правилами консеквенции.
Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор — тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода
{Р}{Р}. (2.32)
Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р
{PXe}x:=e{P}. (2.33)
Здесь утверждается, что если Р истинно для подстановки е вместо х перед выполнением присваивания, то Р должно быть истинным, когда переменной х присвоили ее новое значение. Это правило лучше пояснить примерами, данными на рис. 2Б.
2.4. СОСТАВНЫЕ И УСЛОВНЫЕ ОПЕРАТОРЫ
Предположим, мы хотим доказать, что имеет место {Р} S {Q}, когда S является структурным оператором. Нам необходимо правило для каждого типа композиции операторов, которое позволит вывести свойства сложного (структурного) оператора на основе установленных свойств его компонент. В этом разделе обсуждаются такие правила для составных и условных операторов.
Составные операторы.
Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состо-
ящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)
и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).
Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:
{Р} S, [R], {R} S, {Q}
{Р}begin Si;S, end {Q} (2-36)
Правило вывода (2.36) обобщается следующим очевидным образом:
{Рi-1}S1{Pi} дпя i=1,....n
{P0} begin S1;. ..Sn. end {Pn}
Условные операторы.
Если S1 и S2 - операторы, а В — Булево выражение (т.е. выражение, имеющее значение Булевого типа), то
if В then S1 else S2 (2.38)
есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае — действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).
Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность [Р] if В then S1 else S2 {Q},то необходимо доказать два утверждения.
1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.
2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^
В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^
b}s2{q].
Если мы доказали как [Р^В] S1 {Q}, так и{Р^
В} S2 {Q}, то можно утверждать, что если Р справедливо перед выполнением (2.38), то Q будет справедливо по окончании его выполнения независимо от того, какой оператор (S1 или S2) был выбран для выполнения. Итак, можно сформулировать следующее правило вывода:
{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^
BQ .
{Р} 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/\
В .Р, то, следовательно, Р удовлетворится при достижении точки А во второй раз (если это вообще происходит). Но тогда вновь на основании [Р] S {Q} будет удовлетворяться Q, когда точка С достигается во второй раз, и т.д. Итак, видно, что при сделанных предположениях Р будет истинно всякий раз, когда достигается точка А, и Q будет истинно всякий раз, когда достигается точка С, независимо от числа повторений цикла. Когда итерационный процесс заканчивается, т.е. когда достигается точка выхода D на рис. 2К, то должно быть истинно утверждение Q^B. Это рассуждение приводит к следующему правилу вывода:
{P}S{Q},Q^
BP
{Р} 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^
BP,{P}S[Q}
{Q^
B}S{Q]
комбинация которого с (2.56) дает
{P}S{Q},Q^
BP
{Q} while
В do S {Q ^ В}
Затем, используя (2.54), получаем искомый результат
[p}s{q},q^
bp
{Р} 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
begin r : = r — у;
q:=1+q
end end {(x=q*y+r)^(0<=r
Критерий корректности (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). Но правило вывода
Правила (2.27) и (2.30) называются правилами консеквенции.
Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор — тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода
{Р}{Р}. (2.32)
Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р
{PXe}x:=e{P}. (2.33)
Здесь утверждается, что если Р истинно для подстановки е вместо х перед выполнением присваивания, то Р должно быть истинным, когда переменной х присвоили ее новое значение. Это правило лучше пояснить примерами, данными на рис. 2Б.
2.4. СОСТАВНЫЕ И УСЛОВНЫЕ ОПЕРАТОРЫ
Предположим, мы хотим доказать, что имеет место {Р} S {Q}, когда S является структурным оператором. Нам необходимо правило для каждого типа композиции операторов, которое позволит вывести свойства сложного (структурного) оператора на основе установленных свойств его компонент. В этом разделе обсуждаются такие правила для составных и условных операторов.
Составные операторы.
Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состо-
ящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)
и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).
Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:
{Р} S, [R], {R} S, {Q}
{Р}begin Si;S, end {Q} (2-36)
Правило вывода (2.36) обобщается следующим очевидным образом:
{Рi-1}S1{Pi} дпя i=1,....n
{P0} begin S1;. ..Sn. end {Pn}
Условные операторы.
Если S1 и S2 - операторы, а В — Булево выражение (т.е. выражение, имеющее значение Булевого типа), то
if В then S1 else S2 (2.38)
есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае — действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).
Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность [Р] if В then S1 else S2 {Q},то необходимо доказать два утверждения.
1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.
2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^
В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^
b}s2{q].
Если мы доказали как [Р^В] S1 {Q}, так и{Р^
В} S2 {Q}, то можно утверждать, что если Р справедливо перед выполнением (2.38), то Q будет справедливо по окончании его выполнения независимо от того, какой оператор (S1 или S2) был выбран для выполнения. Итак, можно сформулировать следующее правило вывода:
{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^
BQ .
{Р} 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/\
В .Р, то, следовательно, Р удовлетворится при достижении точки А во второй раз (если это вообще происходит). Но тогда вновь на основании [Р] S {Q} будет удовлетворяться Q, когда точка С достигается во второй раз, и т.д. Итак, видно, что при сделанных предположениях Р будет истинно всякий раз, когда достигается точка А, и Q будет истинно всякий раз, когда достигается точка С, независимо от числа повторений цикла. Когда итерационный процесс заканчивается, т.е. когда достигается точка выхода D на рис. 2К, то должно быть истинно утверждение Q^B. Это рассуждение приводит к следующему правилу вывода:
{P}S{Q},Q^
BP
{Р} 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^
BP,{P}S[Q}
{Q^
B}S{Q]
комбинация которого с (2.56) дает
{P}S{Q},Q^
BP
{Q} while
В do S {Q ^ В}
Затем, используя (2.54), получаем искомый результат
[p}s{q},q^
bp
{Р} 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
begin r : = r — у;
q:=1+q
end end {(x=q*y+r)^(0<=r
Критерий корректности (2.58) выражается соотношением (х= q *у + r) ^ (0 <= r <у), которое должно иметь место при завершении (2.58),
если (х>=0) ^ (у>0) справедливо перед выполнением (2.58). Это мы и должны доказать.
Рассмотрим сначала цикл в нашей программе, представленный Sз на рис. 2.2 в (рис. 2М). В этом примере В имеет вид (r>= у). Если теперь заметить, что выходное соотношение на рис. 2.2в может быть переписано как
(х=q*у+r)^(r>=0)^
(r>=у), то ясно, что это как раз и есть Р ^
Правила (2.27) и (2.30) называются правилами консеквенции.
Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор — тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода
{Р}{Р}. (2.32)
Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р
{PXe}x:=e{P}. (2.33)
Здесь утверждается, что если Р истинно для подстановки е вместо х перед выполнением присваивания, то Р должно быть истинным, когда переменной х присвоили ее новое значение. Это правило лучше пояснить примерами, данными на рис. 2Б.
2.4. СОСТАВНЫЕ И УСЛОВНЫЕ ОПЕРАТОРЫ
Предположим, мы хотим доказать, что имеет место {Р} S {Q}, когда S является структурным оператором. Нам необходимо правило для каждого типа композиции операторов, которое позволит вывести свойства сложного (структурного) оператора на основе установленных свойств его компонент. В этом разделе обсуждаются такие правила для составных и условных операторов.
Составные операторы.
Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состо-
ящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)
и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).
Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:
{Р} S, [R], {R} S, {Q}
{Р}begin Si;S, end {Q} (2-36)
Правило вывода (2.36) обобщается следующим очевидным образом:
{Рi-1}S1{Pi} дпя i=1,....n
{P0} begin S1;. ..Sn. end {Pn}
Условные операторы.
Если S1 и S2 - операторы, а В — Булево выражение (т.е. выражение, имеющее значение Булевого типа), то
if В then S1 else S2 (2.38)
есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае — действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).
Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность [Р] if В then S1 else S2 {Q},то необходимо доказать два утверждения.
1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.
2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^
В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^
b}s2{q].
Если мы доказали как [Р^В] S1 {Q}, так и{Р^
В} S2 {Q}, то можно утверждать, что если Р справедливо перед выполнением (2.38), то Q будет справедливо по окончании его выполнения независимо от того, какой оператор (S1 или S2) был выбран для выполнения. Итак, можно сформулировать следующее правило вывода:
{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^
BQ .
{Р} 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/\
В .Р, то, следовательно, Р удовлетворится при достижении точки А во второй раз (если это вообще происходит). Но тогда вновь на основании [Р] S {Q} будет удовлетворяться Q, когда точка С достигается во второй раз, и т.д. Итак, видно, что при сделанных предположениях Р будет истинно всякий раз, когда достигается точка А, и Q будет истинно всякий раз, когда достигается точка С, независимо от числа повторений цикла. Когда итерационный процесс заканчивается, т.е. когда достигается точка выхода D на рис. 2К, то должно быть истинно утверждение Q^B. Это рассуждение приводит к следующему правилу вывода:
{P}S{Q},Q^
BP
{Р} 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^
BP,{P}S[Q}
{Q^
B}S{Q]
комбинация которого с (2.56) дает
{P}S{Q},Q^
BP
{Q} while
В do S {Q ^ В}
Затем, используя (2.54), получаем искомый результат
[p}s{q},q^
bp
Правила (2.27) и (2.30) называются правилами консеквенции.
Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор — тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода
{Р}{Р}. (2.32)
Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р
{PXe}x:=e{P}. (2.33)
Здесь утверждается, что если Р истинно для подстановки е вместо х перед выполнением присваивания, то Р должно быть истинным, когда переменной х присвоили ее новое значение. Это правило лучше пояснить примерами, данными на рис. 2Б.
2.4. СОСТАВНЫЕ И УСЛОВНЫЕ ОПЕРАТОРЫ
Предположим, мы хотим доказать, что имеет место {Р} S {Q}, когда S является структурным оператором. Нам необходимо правило для каждого типа композиции операторов, которое позволит вывести свойства сложного (структурного) оператора на основе установленных свойств его компонент. В этом разделе обсуждаются такие правила для составных и условных операторов.
Составные операторы.
Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состо-
ящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)
и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).
Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:
{Р} S, [R], {R} S, {Q}
{Р}begin Si;S, end {Q} (2-36)
Правило вывода (2.36) обобщается следующим очевидным образом:
{Рi-1}S1{Pi} дпя i=1,....n
{P0} begin S1;. ..Sn. end {Pn}
Условные операторы.
Если S1 и S2 - операторы, а В — Булево выражение (т.е. выражение, имеющее значение Булевого типа), то
if В then S1 else S2 (2.38)
есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае — действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).
Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность [Р] if В then S1 else S2 {Q},то необходимо доказать два утверждения.
1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.
2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^
В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^
b}s2{q].
Если мы доказали как [Р^В] S1 {Q}, так и{Р^
В} S2 {Q}, то можно утверждать, что если Р справедливо перед выполнением (2.38), то Q будет справедливо по окончании его выполнения независимо от того, какой оператор (S1 или S2) был выбран для выполнения. Итак, можно сформулировать следующее правило вывода:
{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^
BQ .
{Р} 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/\
В .Р, то, следовательно, Р удовлетворится при достижении точки А во второй раз (если это вообще происходит). Но тогда вновь на основании [Р] S {Q} будет удовлетворяться Q, когда точка С достигается во второй раз, и т.д. Итак, видно, что при сделанных предположениях Р будет истинно всякий раз, когда достигается точка А, и Q будет истинно всякий раз, когда достигается точка С, независимо от числа повторений цикла. Когда итерационный процесс заканчивается, т.е. когда достигается точка выхода D на рис. 2К, то должно быть истинно утверждение Q^B. Это рассуждение приводит к следующему правилу вывода:
{P}S{Q},Q^
BP
{Р} 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^
BP,{P}S[Q}
{Q^
B}S{Q]
комбинация которого с (2.56) дает
{P}S{Q},Q^
BP
Правила (2.27) и (2.30) называются правилами консеквенции.
Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор — тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода
{Р}{Р}. (2.32)
Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р
{PXe}x:=e{P}. (2.33)
Здесь утверждается, что если Р истинно для подстановки е вместо х перед выполнением присваивания, то Р должно быть истинным, когда переменной х присвоили ее новое значение. Это правило лучше пояснить примерами, данными на рис. 2Б.
2.4. СОСТАВНЫЕ И УСЛОВНЫЕ ОПЕРАТОРЫ
Предположим, мы хотим доказать, что имеет место {Р} S {Q}, когда S является структурным оператором. Нам необходимо правило для каждого типа композиции операторов, которое позволит вывести свойства сложного (структурного) оператора на основе установленных свойств его компонент. В этом разделе обсуждаются такие правила для составных и условных операторов.
Составные операторы.
Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состо-
ящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)
и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).
Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:
{Р} S, [R], {R} S, {Q}
{Р}begin Si;S, end {Q} (2-36)
Правило вывода (2.36) обобщается следующим очевидным образом:
{Рi-1}S1{Pi} дпя i=1,....n
{P0} begin S1;. ..Sn. end {Pn}
Условные операторы.
Если S1 и S2 - операторы, а В — Булево выражение (т.е. выражение, имеющее значение Булевого типа), то
if В then S1 else S2 (2.38)
есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае — действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).
Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность [Р] if В then S1 else S2 {Q},то необходимо доказать два утверждения.
1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.
2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^
В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^
b}s2{q].
Если мы доказали как [Р^В] S1 {Q}, так и{Р^
В} S2 {Q}, то можно утверждать, что если Р справедливо перед выполнением (2.38), то Q будет справедливо по окончании его выполнения независимо от того, какой оператор (S1 или S2) был выбран для выполнения. Итак, можно сформулировать следующее правило вывода:
{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^
BQ .
{Р} 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/\
В .Р, то, следовательно, Р удовлетворится при достижении точки А во второй раз (если это вообще происходит). Но тогда вновь на основании [Р] S {Q} будет удовлетворяться Q, когда точка С достигается во второй раз, и т.д. Итак, видно, что при сделанных предположениях Р будет истинно всякий раз, когда достигается точка А, и Q будет истинно всякий раз, когда достигается точка С, независимо от числа повторений цикла. Когда итерационный процесс заканчивается, т.е. когда достигается точка выхода D на рис. 2К, то должно быть истинно утверждение Q^B. Это рассуждение приводит к следующему правилу вывода:
{P}S{Q},Q^
BP
{Р} 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^
BP,{P}S[Q}
Правила (2.27) и (2.30) называются правилами консеквенции.
Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор — тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода
{Р}{Р}. (2.32)
Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р
{PXe}x:=e{P}. (2.33)
Здесь утверждается, что если Р истинно для подстановки е вместо х перед выполнением присваивания, то Р должно быть истинным, когда переменной х присвоили ее новое значение. Это правило лучше пояснить примерами, данными на рис. 2Б.
2.4. СОСТАВНЫЕ И УСЛОВНЫЕ ОПЕРАТОРЫ
Предположим, мы хотим доказать, что имеет место {Р} S {Q}, когда S является структурным оператором. Нам необходимо правило для каждого типа композиции операторов, которое позволит вывести свойства сложного (структурного) оператора на основе установленных свойств его компонент. В этом разделе обсуждаются такие правила для составных и условных операторов.
Составные операторы.
Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состо-
ящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)
и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).
Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:
{Р} S, [R], {R} S, {Q}
{Р}begin Si;S, end {Q} (2-36)
Правило вывода (2.36) обобщается следующим очевидным образом:
{Рi-1}S1{Pi} дпя i=1,....n
{P0} begin S1;. ..Sn. end {Pn}
Условные операторы.
Если S1 и S2 - операторы, а В — Булево выражение (т.е. выражение, имеющее значение Булевого типа), то
if В then S1 else S2 (2.38)
есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае — действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).
Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность [Р] if В then S1 else S2 {Q},то необходимо доказать два утверждения.
1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.
2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^
В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^
b}s2{q].
Если мы доказали как [Р^В] S1 {Q}, так и{Р^
В} S2 {Q}, то можно утверждать, что если Р справедливо перед выполнением (2.38), то Q будет справедливо по окончании его выполнения независимо от того, какой оператор (S1 или S2) был выбран для выполнения. Итак, можно сформулировать следующее правило вывода:
{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^
BQ .
{Р} 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/\
В .Р, то, следовательно, Р удовлетворится при достижении точки А во второй раз (если это вообще происходит). Но тогда вновь на основании [Р] S {Q} будет удовлетворяться Q, когда точка С достигается во второй раз, и т.д. Итак, видно, что при сделанных предположениях Р будет истинно всякий раз, когда достигается точка А, и Q будет истинно всякий раз, когда достигается точка С, независимо от числа повторений цикла. Когда итерационный процесс заканчивается, т.е. когда достигается точка выхода D на рис. 2К, то должно быть истинно утверждение Q^B. Это рассуждение приводит к следующему правилу вывода:
{P}S{Q},Q^
BP
{Р} 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 ^ В}
где применяется равенство
Правила (2.27) и (2.30) называются правилами консеквенции.
Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор — тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода
{Р}{Р}. (2.32)
Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р
{PXe}x:=e{P}. (2.33)
Здесь утверждается, что если Р истинно для подстановки е вместо х перед выполнением присваивания, то Р должно быть истинным, когда переменной х присвоили ее новое значение. Это правило лучше пояснить примерами, данными на рис. 2Б.
2.4. СОСТАВНЫЕ И УСЛОВНЫЕ ОПЕРАТОРЫ
Предположим, мы хотим доказать, что имеет место {Р} S {Q}, когда S является структурным оператором. Нам необходимо правило для каждого типа композиции операторов, которое позволит вывести свойства сложного (структурного) оператора на основе установленных свойств его компонент. В этом разделе обсуждаются такие правила для составных и условных операторов.
Составные операторы.
Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состо-
ящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)
и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).
Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:
{Р} S, [R], {R} S, {Q}
{Р}begin Si;S, end {Q} (2-36)
Правило вывода (2.36) обобщается следующим очевидным образом:
{Рi-1}S1{Pi} дпя i=1,....n
{P0} begin S1;. ..Sn. end {Pn}
Условные операторы.
Если S1 и S2 - операторы, а В — Булево выражение (т.е. выражение, имеющее значение Булевого типа), то
if В then S1 else S2 (2.38)
есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае — действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).
Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность [Р] if В then S1 else S2 {Q},то необходимо доказать два утверждения.
1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.
2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^
В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^
b}s2{q].
Если мы доказали как [Р^В] S1 {Q}, так и{Р^
В} S2 {Q}, то можно утверждать, что если Р справедливо перед выполнением (2.38), то Q будет справедливо по окончании его выполнения независимо от того, какой оператор (S1 или S2) был выбран для выполнения. Итак, можно сформулировать следующее правило вывода:
{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^
BQ .
{Р} 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/\
В .Р, то, следовательно, Р удовлетворится при достижении точки А во второй раз (если это вообще происходит). Но тогда вновь на основании [Р] S {Q} будет удовлетворяться Q, когда точка С достигается во второй раз, и т.д. Итак, видно, что при сделанных предположениях Р будет истинно всякий раз, когда достигается точка А, и Q будет истинно всякий раз, когда достигается точка С, независимо от числа повторений цикла. Когда итерационный процесс заканчивается, т.е. когда достигается точка выхода D на рис. 2К, то должно быть истинно утверждение Q^B. Это рассуждение приводит к следующему правилу вывода:
{P}S{Q},Q^
BP
{Р} 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}
Правила (2.27) и (2.30) называются правилами консеквенции.
Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор — тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода
{Р}{Р}. (2.32)
Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р
{PXe}x:=e{P}. (2.33)
Здесь утверждается, что если Р истинно для подстановки е вместо х перед выполнением присваивания, то Р должно быть истинным, когда переменной х присвоили ее новое значение. Это правило лучше пояснить примерами, данными на рис. 2Б.
2.4. СОСТАВНЫЕ И УСЛОВНЫЕ ОПЕРАТОРЫ
Предположим, мы хотим доказать, что имеет место {Р} S {Q}, когда S является структурным оператором. Нам необходимо правило для каждого типа композиции операторов, которое позволит вывести свойства сложного (структурного) оператора на основе установленных свойств его компонент. В этом разделе обсуждаются такие правила для составных и условных операторов.
Составные операторы.
Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состо-
ящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)
и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).
Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:
{Р} S, [R], {R} S, {Q}
{Р}begin Si;S, end {Q} (2-36)
Правило вывода (2.36) обобщается следующим очевидным образом:
{Рi-1}S1{Pi} дпя i=1,....n
{P0} begin S1;. ..Sn. end {Pn}
Условные операторы.
Если S1 и S2 - операторы, а В — Булево выражение (т.е. выражение, имеющее значение Булевого типа), то
if В then S1 else S2 (2.38)
есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае — действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).
Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность [Р] if В then S1 else S2 {Q},то необходимо доказать два утверждения.
1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.
2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^
В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^
b}s2{q].
Если мы доказали как [Р^В] S1 {Q}, так и{Р^
В} S2 {Q}, то можно утверждать, что если Р справедливо перед выполнением (2.38), то Q будет справедливо по окончании его выполнения независимо от того, какой оператор (S1 или S2) был выбран для выполнения. Итак, можно сформулировать следующее правило вывода:
{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^
BQ .
{Р} 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/\
В .Р, то, следовательно, Р удовлетворится при достижении точки А во второй раз (если это вообще происходит). Но тогда вновь на основании [Р] S {Q} будет удовлетворяться Q, когда точка С достигается во второй раз, и т.д. Итак, видно, что при сделанных предположениях Р будет истинно всякий раз, когда достигается точка А, и Q будет истинно всякий раз, когда достигается точка С, независимо от числа повторений цикла. Когда итерационный процесс заканчивается, т.е. когда достигается точка выхода D на рис. 2К, то должно быть истинно утверждение Q^B. Это рассуждение приводит к следующему правилу вывода:
{P}S{Q},Q^
BP
{Р} 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}
Правила (2.27) и (2.30) называются правилами консеквенции.
Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор — тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода
{Р}{Р}. (2.32)
Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р
{PXe}x:=e{P}. (2.33)
Здесь утверждается, что если Р истинно для подстановки е вместо х перед выполнением присваивания, то Р должно быть истинным, когда переменной х присвоили ее новое значение. Это правило лучше пояснить примерами, данными на рис. 2Б.
2.4. СОСТАВНЫЕ И УСЛОВНЫЕ ОПЕРАТОРЫ
Предположим, мы хотим доказать, что имеет место {Р} S {Q}, когда S является структурным оператором. Нам необходимо правило для каждого типа композиции операторов, которое позволит вывести свойства сложного (структурного) оператора на основе установленных свойств его компонент. В этом разделе обсуждаются такие правила для составных и условных операторов.
Составные операторы.
Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состо-
ящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)
и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).
Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:
{Р} S, [R], {R} S, {Q}
{Р}begin Si;S, end {Q} (2-36)
Правило вывода (2.36) обобщается следующим очевидным образом:
{Рi-1}S1{Pi} дпя i=1,....n
{P0} begin S1;. ..Sn. end {Pn}
Условные операторы.
Если S1 и S2 - операторы, а В — Булево выражение (т.е. выражение, имеющее значение Булевого типа), то
if В then S1 else S2 (2.38)
есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае — действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).
Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность [Р] if В then S1 else S2 {Q},то необходимо доказать два утверждения.
1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.
2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^
В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^
b}s2{q].
Если мы доказали как [Р^В] S1 {Q}, так и{Р^
В} S2 {Q}, то можно утверждать, что если Р справедливо перед выполнением (2.38), то Q будет справедливо по окончании его выполнения независимо от того, какой оператор (S1 или S2) был выбран для выполнения. Итак, можно сформулировать следующее правило вывода:
{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^
BQ .
{Р} 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/\
В .Р, то, следовательно, Р удовлетворится при достижении точки А во второй раз (если это вообще происходит). Но тогда вновь на основании [Р] S {Q} будет удовлетворяться Q, когда точка С достигается во второй раз, и т.д. Итак, видно, что при сделанных предположениях Р будет истинно всякий раз, когда достигается точка А, и Q будет истинно всякий раз, когда достигается точка С, независимо от числа повторений цикла. Когда итерационный процесс заканчивается, т.е. когда достигается точка выхода D на рис. 2К, то должно быть истинно утверждение Q^B. Это рассуждение приводит к следующему правилу вывода:
{P}S{Q},Q^
BP
Правила (2.27) и (2.30) называются правилами консеквенции.
Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор — тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода
{Р}{Р}. (2.32)
Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р
{PXe}x:=e{P}. (2.33)
Здесь утверждается, что если Р истинно для подстановки е вместо х перед выполнением присваивания, то Р должно быть истинным, когда переменной х присвоили ее новое значение. Это правило лучше пояснить примерами, данными на рис. 2Б.
2.4. СОСТАВНЫЕ И УСЛОВНЫЕ ОПЕРАТОРЫ
Предположим, мы хотим доказать, что имеет место {Р} S {Q}, когда S является структурным оператором. Нам необходимо правило для каждого типа композиции операторов, которое позволит вывести свойства сложного (структурного) оператора на основе установленных свойств его компонент. В этом разделе обсуждаются такие правила для составных и условных операторов.
Составные операторы.
Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состо-
ящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)
и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).
Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:
{Р} S, [R], {R} S, {Q}
{Р}begin Si;S, end {Q} (2-36)
Правило вывода (2.36) обобщается следующим очевидным образом:
{Рi-1}S1{Pi} дпя i=1,....n
{P0} begin S1;. ..Sn. end {Pn}
Условные операторы.
Если S1 и S2 - операторы, а В — Булево выражение (т.е. выражение, имеющее значение Булевого типа), то
if В then S1 else S2 (2.38)
есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае — действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).
Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность [Р] if В then S1 else S2 {Q},то необходимо доказать два утверждения.
1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.
2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^
В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^
b}s2{q].
Если мы доказали как [Р^В] S1 {Q}, так и{Р^
В} S2 {Q}, то можно утверждать, что если Р справедливо перед выполнением (2.38), то Q будет справедливо по окончании его выполнения независимо от того, какой оператор (S1 или S2) был выбран для выполнения. Итак, можно сформулировать следующее правило вывода:
{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^
BQ .
{Р} 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/\
Правила (2.27) и (2.30) называются правилами консеквенции.
Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор — тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода
{Р}{Р}. (2.32)
Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р
{PXe}x:=e{P}. (2.33)
Здесь утверждается, что если Р истинно для подстановки е вместо х перед выполнением присваивания, то Р должно быть истинным, когда переменной х присвоили ее новое значение. Это правило лучше пояснить примерами, данными на рис. 2Б.
2.4. СОСТАВНЫЕ И УСЛОВНЫЕ ОПЕРАТОРЫ
Предположим, мы хотим доказать, что имеет место {Р} S {Q}, когда S является структурным оператором. Нам необходимо правило для каждого типа композиции операторов, которое позволит вывести свойства сложного (структурного) оператора на основе установленных свойств его компонент. В этом разделе обсуждаются такие правила для составных и условных операторов.
Составные операторы.
Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состо-
ящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)
и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).
Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:
{Р} S, [R], {R} S, {Q}
{Р}begin Si;S, end {Q} (2-36)
Правило вывода (2.36) обобщается следующим очевидным образом:
{Рi-1}S1{Pi} дпя i=1,....n
{P0} begin S1;. ..Sn. end {Pn}
Условные операторы.
Если S1 и S2 - операторы, а В — Булево выражение (т.е. выражение, имеющее значение Булевого типа), то
if В then S1 else S2 (2.38)
есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае — действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).
Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность [Р] if В then S1 else S2 {Q},то необходимо доказать два утверждения.
1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.
2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^
В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^
b}s2{q].
Если мы доказали как [Р^В] S1 {Q}, так и{Р^
В} S2 {Q}, то можно утверждать, что если Р справедливо перед выполнением (2.38), то Q будет справедливо по окончании его выполнения независимо от того, какой оператор (S1 или S2) был выбран для выполнения. Итак, можно сформулировать следующее правило вывода:
{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^
BQ .
{Р} 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.27) и (2.30) называются правилами консеквенции.
Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор — тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода
{Р}{Р}. (2.32)
Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р
{PXe}x:=e{P}. (2.33)
Здесь утверждается, что если Р истинно для подстановки е вместо х перед выполнением присваивания, то Р должно быть истинным, когда переменной х присвоили ее новое значение. Это правило лучше пояснить примерами, данными на рис. 2Б.
2.4. СОСТАВНЫЕ И УСЛОВНЫЕ ОПЕРАТОРЫ
Предположим, мы хотим доказать, что имеет место {Р} S {Q}, когда S является структурным оператором. Нам необходимо правило для каждого типа композиции операторов, которое позволит вывести свойства сложного (структурного) оператора на основе установленных свойств его компонент. В этом разделе обсуждаются такие правила для составных и условных операторов.
Составные операторы.
Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состо-
ящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)
и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).
Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:
{Р} S, [R], {R} S, {Q}
{Р}begin Si;S, end {Q} (2-36)
Правило вывода (2.36) обобщается следующим очевидным образом:
{Рi-1}S1{Pi} дпя i=1,....n
{P0} begin S1;. ..Sn. end {Pn}
Условные операторы.
Если S1 и S2 - операторы, а В — Булево выражение (т.е. выражение, имеющее значение Булевого типа), то
if В then S1 else S2 (2.38)
есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае — действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).
Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность [Р] if В then S1 else S2 {Q},то необходимо доказать два утверждения.
1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.
2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^
В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^
b}s2{q].
Если мы доказали как [Р^В] S1 {Q}, так и{Р^
В} S2 {Q}, то можно утверждать, что если Р справедливо перед выполнением (2.38), то Q будет справедливо по окончании его выполнения независимо от того, какой оператор (S1 или S2) был выбран для выполнения. Итак, можно сформулировать следующее правило вывода:
{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^
BQ .
Правила (2.27) и (2.30) называются правилами консеквенции.
Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор — тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода
{Р}{Р}. (2.32)
Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р
{PXe}x:=e{P}. (2.33)
Здесь утверждается, что если Р истинно для подстановки е вместо х перед выполнением присваивания, то Р должно быть истинным, когда переменной х присвоили ее новое значение. Это правило лучше пояснить примерами, данными на рис. 2Б.
2.4. СОСТАВНЫЕ И УСЛОВНЫЕ ОПЕРАТОРЫ
Предположим, мы хотим доказать, что имеет место {Р} S {Q}, когда S является структурным оператором. Нам необходимо правило для каждого типа композиции операторов, которое позволит вывести свойства сложного (структурного) оператора на основе установленных свойств его компонент. В этом разделе обсуждаются такие правила для составных и условных операторов.
Составные операторы.
Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состо-
ящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)
и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).
Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:
{Р} S, [R], {R} S, {Q}
{Р}begin Si;S, end {Q} (2-36)
Правило вывода (2.36) обобщается следующим очевидным образом:
{Рi-1}S1{Pi} дпя i=1,....n
{P0} begin S1;. ..Sn. end {Pn}
Условные операторы.
Если S1 и S2 - операторы, а В — Булево выражение (т.е. выражение, имеющее значение Булевого типа), то
if В then S1 else S2 (2.38)
есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае — действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).
Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность [Р] if В then S1 else S2 {Q},то необходимо доказать два утверждения.
1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.
2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^
В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^
b}s2{q].
Если мы доказали как [Р^В] S1 {Q}, так и{Р^
В} S2 {Q}, то можно утверждать, что если Р справедливо перед выполнением (2.38), то Q будет справедливо по окончании его выполнения независимо от того, какой оператор (S1 или S2) был выбран для выполнения. Итак, можно сформулировать следующее правило вывода:
{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), то необходимо доказать, что Р ^
Правила (2.27) и (2.30) называются правилами консеквенции.
Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор — тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода
{Р}{Р}. (2.32)
Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р
{PXe}x:=e{P}. (2.33)
Здесь утверждается, что если Р истинно для подстановки е вместо х перед выполнением присваивания, то Р должно быть истинным, когда переменной х присвоили ее новое значение. Это правило лучше пояснить примерами, данными на рис. 2Б.
2.4. СОСТАВНЫЕ И УСЛОВНЫЕ ОПЕРАТОРЫ
Предположим, мы хотим доказать, что имеет место {Р} S {Q}, когда S является структурным оператором. Нам необходимо правило для каждого типа композиции операторов, которое позволит вывести свойства сложного (структурного) оператора на основе установленных свойств его компонент. В этом разделе обсуждаются такие правила для составных и условных операторов.
Составные операторы.
Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состо-
ящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)
и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).
Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:
{Р} S, [R], {R} S, {Q}
{Р}begin Si;S, end {Q} (2-36)
Правило вывода (2.36) обобщается следующим очевидным образом:
{Рi-1}S1{Pi} дпя i=1,....n
{P0} begin S1;. ..Sn. end {Pn}
Условные операторы.
Если S1 и S2 - операторы, а В — Булево выражение (т.е. выражение, имеющее значение Булевого типа), то
if В then S1 else S2 (2.38)
есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае — действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).
Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность [Р] if В then S1 else S2 {Q},то необходимо доказать два утверждения.
1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.
2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^
В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^
b}s2{q].
Если мы доказали как [Р^В] S1 {Q}, так и{Р^
В} S2 {Q}, то можно утверждать, что если Р справедливо перед выполнением (2.38), то Q будет справедливо по окончании его выполнения независимо от того, какой оператор (S1 или S2) был выбран для выполнения. Итак, можно сформулировать следующее правило вывода:
Правила (2.27) и (2.30) называются правилами консеквенции.
Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор — тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода
{Р}{Р}. (2.32)
Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р
{PXe}x:=e{P}. (2.33)
Здесь утверждается, что если Р истинно для подстановки е вместо х перед выполнением присваивания, то Р должно быть истинным, когда переменной х присвоили ее новое значение. Это правило лучше пояснить примерами, данными на рис. 2Б.
2.4. СОСТАВНЫЕ И УСЛОВНЫЕ ОПЕРАТОРЫ
Предположим, мы хотим доказать, что имеет место {Р} S {Q}, когда S является структурным оператором. Нам необходимо правило для каждого типа композиции операторов, которое позволит вывести свойства сложного (структурного) оператора на основе установленных свойств его компонент. В этом разделе обсуждаются такие правила для составных и условных операторов.
Составные операторы.
Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состо-
ящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)
и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).
Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:
{Р} S, [R], {R} S, {Q}
{Р}begin Si;S, end {Q} (2-36)
Правило вывода (2.36) обобщается следующим очевидным образом:
{Рi-1}S1{Pi} дпя i=1,....n
{P0} begin S1;. ..Sn. end {Pn}
Условные операторы.
Если S1 и S2 - операторы, а В — Булево выражение (т.е. выражение, имеющее значение Булевого типа), то
if В then S1 else S2 (2.38)
есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае — действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).
Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность [Р] if В then S1 else S2 {Q},то необходимо доказать два утверждения.
1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.
2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^
В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^{P^B}S1{Q},{P^
{Р} 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), то справедливо не только Р, но и
Заметим, что (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 ^
{Р} repeat S until B{Q^B]
Покажем, как заменить оператор repeat-until структурной схемой, в которой цикл задается оператором while-do. Вспомним идею repeat S until В — выполнить S, а затем проверить В, затем выполнить снова S, если В ложно, и повторять этот процесс. Другими словами, выполнить S, повторяя затем выполнение S до тех пор, пока В не станет истинным. Таким образом, имеем эквивалентность:
repeat Suntil В = begin S; while
и правила вывода
{P}S1{R},{R}S2{Q]
{Р} begin S1; S2 end {Q}' (2.54)
Нам потребуется также правило консеквенции
Р R, {R} S {Q}
{Р} S {Q}
Если задано {Р} S {Q}, то естественно берем Q в качестве соотношения в точке входа в while
{Q} while
{Q^
{Q} while
{Р} begin S; while
{P^B}S{P}
{Р} while В do S {Р ^
Следующий шаг состоит в проверке того, что требуемое условие
{(х >= 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
что мы и хотели доказать. Так как это было доказательство частичной корректности, условие у > 0 не использовалось при доказательстве. Это условие, однако, будет играть существенную роль при доказательстве того, что алгоритм действительно завершается.
Аппаратные средства персональных компьютеров
Создание современных персональных компьютеров (ПК) стало возможным благодаря серьезным научным прорывам в областях материаловедения, микроминиатюризации радиоэлектронных элементов, информатики, робототехники, прикладной математики. За каких-то пять-шесть лет маленькие дешёвые электронные модули полностью заменили огромные стойки, начинённые дорогостоящими компьютерными компонентами, а современный ПК впитал все накопившиеся в вычислительной технике за долгие годы разработки, принципы, идеи.
Однако чисто внешний эффект миниатюризации современных компьютеров ничто по сравнению с их преимуществом над электронно-вычислительными машинами (ЭВМ) предыдущих поколений (серии ЕС ЭВМ, СМ и т.д.). Прежде всего, это возросшая во много раз производительность, малое потребление электроэнергии, дешевизна технического обслуживания и эксплуатации. Компьютеры трансформировались из ЭВМ, занимавших пространства площадью свыше 100 м2, в ПК, которые размещаются теперь на рабочих столах и даже в карманах пиджаков пользователей.
История создания персонального компьютера
В истории вычислительной техники можно выделить два больших этапа развития. Для первого этапа характерно применение в компьютерах не микросхем, а радиоламп и транзисторов, не оперативной памяти на динамических элементах, а памяти на ферритовых кольцах, не миниатюрных накопителей на магнитных дисках, а огромных стоек с накопителями на сменных магнитных дисках.
Второй этап развития компьютерной техники ознаменовался началом выпуска ЭВМ на модулях микропроцессоров. В 1971 г. был выпущен первый 4-разрядный микропроцессор Intel 4004, который обладал рядом положительных особенностей, свойственных современным микропроцессорам, - универсальностью, гибкостью, миниатюрностью, малой потребляемой мощностью и низкой стоимостью. Подобные микропроцессоры свыше десятилетия использовались как в зарубежной, так и в отечественной вычислительной технике.
Первыми персональными компьютерами принято считать микроЭВМ Altair 8800 производства MITS, которые поступили в продажу в 1975 г. в виде наборов для радиолюбителей "Сделай сам". В этих компьютерах использовались интегральные микросхемы малой (до 100 транзисторов на кристалл) и средней (до 1000 транзисторов на кристалл) степени интеграции, а также 8-разрядный микропроцессор Intel 8080.
В 1977 г. корпорация Apple выпустила в продажу персональный компьютер Apple II, который отличался совершенным (по тем временам) программным обеспечением, рассчитанным на самых неподготовленных пользователей. Простота освоения работы на компьютере позволяла использовать эту технику не только специалистам-радиолюбителям и профессионалам, но и всем желающим приобщиться к миру электроники. Компьютер Apple II был собран на микросхемах средней степени интеграции и имел микропроцессор Motorola 6800.
Начало 80-х знаменуется разделением мира ПК на две фракции, несовместимых друг с другом ПК, - Macintosh (наследники Apple II) и IBM PC. Первые ПЭВМ имели существенные недостатки, ограничивающие распространение ПК в среде неподготовленных пользователей и, в основном, отвечали интересам узкого круга профессионалов. Все они имели закрытую архитектуру. Это означает, что аппаратные средства были представлены одним неразъемным устройством. Совершенствование компьютера было уделом профессионалов-разработчиков. В августе 1981 года фирма IBM выпустила первый ПК, в котором осуществила модульный принцип построения, использовавшийся до этого в больших вычислительных системах. Такое построение, называющееся открытой архитектурой, обеспечивало возможность сборки ЭВМ из независимо изготовленных частей. На системной (материнской) плате размещены только те блоки, которые осуществляют обработку информации. Схемы, управляющие всеми остальными устройствами компьютера, реализованы на отдельных платах, которые вставляются в стандартные разъемы на системной плате - слоты. Это позволяет легко заменять дополнительные устройства на новые при старении прежних, увеличивать объем памяти, добавлять, по мере необходимости, новые устройства.
Начиная с 1981 г. лидерство на компьютерном рынке захватила корпорация IBM с компьютером IBM PC, который в дальнейшем стал стандартом для производителей персональных компьютеров. Эти ПК разрабатывались на базе 8-разрядного процессора Intel 8088. Первые IBM PC имели динамическую память 256 Кбайт, источники питания мощностью 63,5 Вт и накопители на двусторонних гибких магнитных дисках (НГМД) на 360 Кбайт.
В 1983 г. фирма IBM представила расширенный (eXTended) вариант персонального компьютера IBM PC XT. В этой модели появился накопитель на жестких магнитных дисках (НЖМД) на 10 или 20 Мбайт, двусторонние НГМД на 360 Кбайт (5,25 дюйма) или 720 Кбайт (3,5 дюйма), а ёмкость оперативной памяти была расширена до 640 Кбайт. Все модели IBM PC XT обладали более мощными источниками питания (до 150 Вт) и располагали 8-разрядным микропроцессором Intel 8088 и сопроцессором Intel 8087.
В 1984 г. фирма IBM предложила открытый стандарт IBM PC Advanced Technologies (AT), который, как и все предыдущие, был открыт для дублирования всеми ведущими корпорациями-производителями компьютеров. IBM PC AT были разработаны на базе новых 16-разрядных процессоров Intel 80286, которые по сравнению с Intel 8088 имели несколько новых режимов работы. В AT использовался новый сопроцессор Intel 80287. Кроме того, элементная база обрамления процессора впервые содержала модули комплектов микросхем (так называемых чипсетов) с очень высокой степенью интеграции (свыше 100 000 транзисторов на кристалл). ПК IBM PC AT располагал мощным блоком питания (200 Вт), жестким диском (30 Мбайт), оперативной динамической памятью 640 Кбайт с возможностью расширения до 1 Мбайт, двусторонними НГМД (360 Кбайт) и 1,2 Мбайт (5,25 дюйма) или 720 Кбайт (3,5 дюйма).
Так как открытый стандарт AT стал достоянием всех фирм, желающих продвигать свои изделия в ряду самых наукоемких продуктов, то фирма IBM утратила лидирующие позиции в мире ПК. Поэтому она предприняла попытку создания закрытого стандарта. В 1987 г. был представлен новый ПК семейства PS/2, модель 25. Основным отличием PS/2 от PC являлось наличие новой 32-разрядной системной архитектуры МСА (Micro Channel Architecture), несовместимой с шиной ISA (Industry Standard Architecture), применявшейся в PC AT. Магистрали МСА имеют более высокие скоростные данные, чем у ISA, кроме того, разъемы расширения шин не совпадают. Впервые IBM интегрировала на материнскую плату некоторые контроллеры - параллельные и последовательные порты, видеоконтроллер.
ПК IBM PS/2 имели успех очень непродолжительное время, поскольку усилиями корпораций-производителей персональных компьютеров семейства PC, в противовес шине МСА, была разработана более технологичная системная архитектура EISA (Enhanced ISA - усовершенствованная шина стандартной промышленной архитектуры). По своим характеристикам она адекватна МСА. Кроме того, разъемы шины позволяли устанавливать не только платы нового формата, но и ISA, что импонировало широкому кругу пользователей, которые в новом компьютере могли бы использовать старые периферийные устройства и не затрачивать средства на покупку новых. Обе шинные архитектуры просуществовали недолго. Стоимость периферийных устройств и компонентов ПК была высока. Продвижение на рынок персональных компьютеров технологии PS/2 было остановлено и в настоящее время доминирующей технологией является IBM PC.
С 1992 г. фирма Intel приступила к массовому внедрению в ПК архитектуры новой шины PCI (Peripheral Component Interconnect - шина расширения интерфейса периферийных компонентов). Она обладает хорошими показателями производительности, не антагонистична по отношению к другим шинам, с которыми может сосуществовать в пределах одной компьютерной системы. Шина расширяема, т.е. допускает использование плат устройств различного уровня интеллекта и производительности, разрядности, напряжений питания. Архитектура шины позволяет внедрять в нее очень существенные доработки, например графическую шину AGP (Accelerated Graphics Port - быстродействующий графический порт), что повышает общее быстродействие системы.
Шина ISA, в отличии от шин МСА и EISA, благополучно существует и ныне, обслуживая медленные периферийные устройства, доставшиеся пользователям от компьютеров AT. Её можно обнаружить в вычислительных системах по соседству с наборами микросхем и процессорами Pentium, превышающими пропускную способность шины ISA в несколько сот раз. Несмотря на еще достаточно живой интерес пользователей к этой шине, она, по рекомендациям спецификации PC-99, будет постепенно изыматься из системы ПК.
Что собой представляют спецификации РС-Х? Для координации усилий разработчиков аппаратного и программного обеспечения в среде Windows ежегодно проводится конференция WinHEC (Windows Hardware Engineering Conference), на которой производители программного обеспечения представляют свои рекомендации разработчикам аппаратных средств. Основными действующими лицами на конференции являются корпорации Intel и Microsoft. В результате дискуссий и обмена мнениями обнародуется очередная, на год-два, версия спецификации РС-Х, имеющая рекомендательный характер. Например, в соответствии с предыдущей спецификацией PC-98 в качестве базовой была принята система с процессором Pentium 200 МГц и 32 Мбайт ОЗУ. В качестве оптимальной была рекомендована видеосистема с разрешающей способностью 1024х768 пикселей. Было положено начало внедрению в ПК последовательной шины IEEE-1394 (FireWire). Ранее, в PC-97, были рассмотрены меры для повсеместной поддержки системной шины PCI и последовательной универсальной шины USB. Спецификация PC-99 расширила возможности ПК за счет применения процессоров с частотой 300 МГц и оперативной памяти 64 Мбайт. Планируется перевод синхронизации системной шины персональных компьютеров на тактовую частоту 100 МГц, внедрение графической шины AGP, новых типов процессоров с 32-разрядной архитектурой.
Компоненты персонального компьютера
Несмотря на разнообразие типов, форм и архитектур персональных компьютеров (рис. 1.1), в составе большинства ПК можно выделить следующие основные устройства: системный блок, монитор, клавиатура, мышь и периферийные устройства. В зависимости от потребностей и возможностей пользователей состав периферии может быть расширен аудиосистемой, модемом, принтером, сканером и т.д.
Системный блок включает все основные составляющие персонального компьютера. Важнейшим его компонентом является материнская (системная) плата (motherboard). Расположенные на ней электронные модули, или чипсеты, а также центральный процессор (ЦП), оперативная память (ОЗУ) составляют базовый комплект электроники компьютера. В системном блоке также размещаются источник питания, устройства внешней памяти - накопители на жестких магнитных дисках (НЖМД), и накопители на гибких магнитных дисках (НГМД). К этой группе устройств в последние годы присоединились дисководы компакт-дисков (CD-ROM-drive), и накопители на сменных магнитных дисках.
К системному блоку подсоединены все внешние устройства: монитор, клавиатура, мышь, принтер, модем, звуковые колонки, сканер и т.д.
Монитор - отображаете на экране текстовую и графическую информацию, вводимые с клавиатуры или выводимые из компьютера данные, сообщения компьютерной системы, копии всевозможных документов и прочую важную для пользователя информацию.
Клавиатура - предназначена для ввода в компьютер команд и данных.
Мышь позволяет указывать на элементы экрана с помощью указателя и путем щелчка на кнопках выполнять определенные операции.
Принтер - выводит в качестве твердой копии текстовую и графическую черно-белую или цветную информацию. Вывод информации осуществляется на бумагу или на пленку.
Модем - предназначен для подключения компьютера к телефонной линии.
Сканер - обеспечивает ввод в ПК текстовой или графической, черно-белой или цветной информации для ее дальнейшей обработки.
Звуковая система - состоит из звуковой карты и звуковых колонок, вынесенных или встроенных в дисплей. Колонки имеют свои усилители и органы регулировки уровня звука.
Архитектура ПК
Архитектура ПК - это структурная схема внутренней организации и взаимодействия основных функциональных модулей компьютера (ЦП, чипсеты, системы памяти персонального компьютера, контроллеры периферийных устройств и сами периферийные устройства). В понятие архитектуры ПК входят также принципы организации вычислительного процесса и переработки информации.
Детальный анализ архитектуры компьютера содержит описание представления программ и данных - систему счисления, информационные форматы и организацию вычислительного и обменного процессов. Он затрагивает также рассмотрение структуры памяти, методики выполнение машинных операций, системы размещения информации в памяти, системы диагностирования и контроля, а также управления вычислительным процессом.
Как видно, архитектура ПК - ёмкое понятие, рассматривающее тонкости взаимодействия всех его компонентов, объясняющее тончайшие нюансы вычислительных и обменных процессов.
На рис. 1.3 изображена упрошенная блок-схема, которая дает общее представление об архитектуре и основных компонентах компьютера.
1 2 3 4 5 6 7