3.3.3. Операторы цикла

Операторы цикла позволяют повторятьвыполнение отдельных частей программы. Оператор вида

while В dо

S

еnd do;

называется оператором цикла whiledо, логическое выражение В -- условием цикла, а последовательность операторов S -- телом цикла. Цикл while-dо означает повторное выполнение S, пока В истинно: сначала вычисляется В;

если его значение ложно (false), то выполнение цикла заканчивается,

в противном случае выполняется S; после чего снова вычисляется значение В и т.д.

Таким образом, если В ложно с самого начала, то S не будет выполняться ни разу.

П р и м е р 3. 10. Для того чтобы вычислить сумму

11 + 22 +...+ nn  , можно воспользоваться следующим циклом:

S:=О; while n>0 do

S:=S+n**n; n:=n-1;

end do;

Теперь определим правило вывода для оператора цикла while do.

Пусть существует такой предикат Р, что

{Р & В} S {Р}

Пусть этот предикат истинен перед выполнением цикла. Тогда если в тот же момент истинно и В, то перед выполнением Б будет истинным и Р & В.

Но тогда после выполнения S опять будет истинным Р. Если при этом В снова истинно, то получаем еще раз истинным Р & В перед новым выполнением S и т.д. Иными словами, Р остается истинным после каждой итерации, поэтому он называется инвариантом цикла. Предикат Р остается истинным и при завершении цикла, когда становится ложным В. Таким образом, получаем следующее правило вывода для оператора цикла while do:

{Р & В} S {Р}

------------------------------------

{P} while В do S end do; {Р & not В}

Наиболее сильный из возможных инвариантов цикла описывает сущность динамических процессов, происходящих при выполнении цикла.

П р и м е р 3. 10 (продолжение).

Какой инвариант y описанного в примере 3.10 цикла? Ясно, что предикат Р = (n>=0) является инвариантом. Однако также ясно, что этот инвариант имеет слабое отношение к основной задаче цикла. На самом деле есть более сильный инвариант:

N

P = (n>=0 & n=<N & S = i**i)

i=n+1

где N-- начальное значение n. Покажем, что

{Р & (n>0)} S:=S+n**n; n:=n+1; {P}

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

N

{P & (n>0)} S:=S+n**n;{n>0 & n=<N & S= i**i }

i=n

N

{n>0 & n=<N & S= i**i } n:=n-1; {P}

i=N

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

N 

(n>0 & n=<N & S=  i**i)S+n**n=

i=n

N

=(n>0 & n=<N & S+n**n=  i**i)=

i=n

N

=(n>0 & n<=N & S=  i**i),

i=n+1

n N

Pn-1 =(n-1>=0 & n-1=<N & S=  i**i)=

i=n

N

= (n>0 & n=<N+1 & S=  i**i),

i=n

и в соответствии со вторым правилом консеквенции

N  n n

(n>0 & n=<N & S=  i**i) => Pn-1 , {Pn-1 } n:=n-1; {P}

i=n

N

{n>0 & n=<N & S=  i**i} n:=n-1; {P}

i=n

Таким образом,

{P & (n>0)} S:=S+n**n; {P}

Очевидно, что перед выпопнением цикла Р=true, если n=N>0.Следовательно, после его выполнения (в соответствии справилом вывода для цикла)

N

(P & not (n>0))=(n=0 & n=<N & S=  i**i)=

i=n+1

N

=(S=  i**i),

i=1

что и требовалось получить в результате выполнения этой программы.

Частичная корректность программы доказана.

Рассмотрим теперь, как доказывать полную корректность программы (ее завершимость за конечное число шагов). Инварианты цикла здесь также играют решающую роль. Пусть t -- целое выражение. Предположим, что

Р & B => (t>0),

и для любого t0, принимающего целые значения,

{Р & В & 0<t=t0} S {0=<t<t0},

Это означает, что (t>=0) также является инвариантом цикла, т.е.значение выражения t остается неотрицательным на каждом шаге выполне-ния цикла. Если при этом спецификация {Р & В} S {Р} доказана, то можноутверждать, что циклический процесс завершен, поскольку t не можетуменьшаться бесконечное число раз и оставаться положительным. Выражение t называют ограничивающей функцией. Таким образом, доказательствозавершимости программы заключается в подборе ограничивающих функцийдля каждом выполняемом цикла. Обычно их легко построить, исходя изспецификаций.