4.1.2 Свойства оператора цикла

Свойство оператора цикла с условием на продолжение можно записать следующим образом:

while$B$do$S$end {~B},

т.е. в момент завершения выполнения оператора возникает состояние памяти, на котором выражение $B$ ложно.

Это свойство соответствует естественному использованию оператора цикла. Нужно получить состояние памяти, удовлетворяющее утверждению $C$, причем известно действие $S$ (это действие, понятно, может описываться структурированным оператором), от которого ожидается, что оно приближает текущее состояние к состоянию, на котором $C$ истинно, и может преобразовать любое начальное состояние за конечное число повторений действия $S$ (это число повторений может быть своим для разных начальных состояний) в состояние, удовлетворяющее $C$. Тогда, взяв в качестве $B$ отрицание $C$, решают задачу с помощью цикла

while$B$do$S$end.

Cправедливо также следующее свойство оператора цикла: если для некоторого утверждения $I$ выполняется

$\{I,B\} S \{ I\}$,

то имеет место

{$I$} while B do S end {$I$}.

Это свойство цикла исключительно важно. Оно отражает тот факт, что если утверждение $I$инвариантно по отношению к оператору $S$ при условии $B$, т.е. если любое выполнение $S$, примененное к состоянию памяти, удовлетворяющему утверждениям $I$ и $B$, не нарушает истинность утверждения $I$, то утверждение $P$ тоже инвариантно по отношению к оператору цикла while$B$do$S$end. Понятие инварианта цикла играет решающую роль в построении итеративных программ, т.е. программ с циклами. При разработке программы условие окончания и инвариант образуют "внешнюю спецификацию" соответствующего циклического участка программы. Всегда, когда это возможно, следует указывать инварианты всех циклов; это повысит наглядность программы, упростит задачу ее анализа.

Фактически имеет место следующее правило вывода свойств оператора цикла с условием на продолжение. Пусть для некоторых утверждений $I$ и $B$ и оператора $S$ имеет место свойство

$\{I,B\} S \{ I\}$.

Тогда справедливо свойство

{$I$} while$B$do$S$end {I, ~B}.

Важно отметить, что расширение языковых средств, описанных в предыдущих главах, оператором цикла с условием на продолжение позволяет достичь достаточной общности и выразительности: комбинируя эти средства, можно выразить все алгоритмические процессы, допустимые для реализации на ЭВМ. При этом рассмотренные правила образования структурированных операторов не лишают программиста возможности рассуждать о программе и доказывать определенные свойства, связанные с выполнениями программы. Поэтому рассмотренные способы структурирования операторов дают естественную основу для разработки программ систематическим образом, исходя на каждом шаге построения из определенных утверждений и получая в конце концов программы, которые правильны по построению.

Вместе с тем нужно иметь в виду следующее. Не существует никакого общего метода, который позволял бы в любых ситуациях доказывать завершимость произвольной программы с циклами. Более точно, нельзя построить алгоритм, который по произвольной итеративной программе P и произвольному набору допустимых входных данных $d$ был бы способен дать ответ, завершается ли программа P, примененная к $d$, или нет. В конкретных практических случаях, однако, проблема доказательства завершимости итеративной программы  поддается решению. Например, можно предложить следующий прием доказательства того, что цикл всегда завершается. Для этого нужно "просто" выделить некоторое такое выражение $Е$E, называемое ограничивающим выражением цикла, значение которого всегда положительно (более точно, нужно доказать, что свойство
E$Е > 0$ всегда выполняется перед выполнением тела цикла и что E$Е \geq 0$ является инвариантом цикла) и которое уменьшается при каждом выполнении тела цикла по крайней мере на единицу. Например, для цикла программы СуммаЭлементовПоследовательности ограничивающим может быть выражение $\mid Input2 \mid$ , а для программы $НаибольшийОбщийДелитель$НаибольшийОбщийДелитель-- выражение $A+B$.
Следует признать, что некоторые циклы уже готовых программ чрезвычайно трудны для понимания и могут потребовать больших интеллектуальных затрат на поиск их инвариантов и ограничивающих выражений. Однако эти затраты по существу и отражают реальную сложность, присутствующую в итеративных программах. Поэтому программист должен проводить доказательство правильности программы во время самого процесса программирования, причем находить инвариант цикла и его ограничивающее выражение до, а не после того, как данный цикл написан.
 

© В.Н. Касьянов, Е.В.Касьянова, 2004