Next:4.1.3
Оператор цикла с условием на продолжение
Up:4.1
Средства для организации
Previous:4.1.1
Оператор цикла с условием на окончание
whiledoend {~B},
т.е. в момент завершения выполнения оператора возникает состояние памяти, на котором выражение ложно.
Это свойство соответствует естественному использованию оператора цикла. Нужно получить состояние памяти, удовлетворяющее утверждению , причем известно действие (это действие, понятно, может описываться структурированным оператором), от которого ожидается, что оно приближает текущее состояние к состоянию, на котором истинно, и может преобразовать любое начальное состояние за конечное число повторений действия (это число повторений может быть своим для разных начальных состояний) в состояние, удовлетворяющее . Тогда, взяв в качестве отрицание , решают задачу с помощью цикла
whiledoend.
Cправедливо также следующее свойство оператора цикла: если для некоторого утверждения выполняется
,
то имеет место
{} while B do S end {}.
Это свойство цикла исключительно важно. Оно отражает тот факт, что если утверждение инвариантно по отношению к оператору при условии , т.е. если любое выполнение , примененное к состоянию памяти, удовлетворяющему утверждениям и , не нарушает истинность утверждения , то утверждение тоже инвариантно по отношению к оператору цикла whiledoend. Понятие инварианта цикла играет решающую роль в построении итеративных программ, т.е. программ с циклами. При разработке программы условие окончания и инвариант образуют "внешнюю спецификацию" соответствующего циклического участка программы. Всегда, когда это возможно, следует указывать инварианты всех циклов; это повысит наглядность программы, упростит задачу ее анализа.
Фактически имеет место следующее правило вывода свойств оператора цикла с условием на продолжение. Пусть для некоторых утверждений и и оператора имеет место свойство
.
Тогда справедливо свойство
{} whiledoend {I, ~B}.
Важно отметить, что расширение языковых средств, описанных в предыдущих главах, оператором цикла с условием на продолжение позволяет достичь достаточной общности и выразительности: комбинируя эти средства, можно выразить все алгоритмические процессы, допустимые для реализации на ЭВМ. При этом рассмотренные правила образования структурированных операторов не лишают программиста возможности рассуждать о программе и доказывать определенные свойства, связанные с выполнениями программы. Поэтому рассмотренные способы структурирования операторов дают естественную основу для разработки программ систематическим образом, исходя на каждом шаге построения из определенных утверждений и получая в конце концов программы, которые правильны по построению.
Вместе с тем нужно иметь в виду следующее. Не существует никакого общего
метода, который позволял бы в любых ситуациях доказывать завершимость произвольной
программы с циклами. Более точно, нельзя построить алгоритм, который по
произвольной итеративной программе P и произвольному набору допустимых
входных данных
был бы способен дать ответ, завершается ли программа P, примененная
к ,
или нет. В конкретных практических случаях, однако, проблема доказательства
завершимости итеративной программы поддается решению. Например, можно
предложить следующий прием доказательства того, что цикл всегда завершается.
Для этого нужно "просто" выделить некоторое такое выражение E,
называемое ограничивающим выражением цикла, значение которого всегда
положительно (более точно, нужно доказать, что свойство
E
всегда выполняется перед выполнением тела цикла и что E
является инвариантом цикла) и которое уменьшается при каждом выполнении
тела цикла по крайней мере на единицу. Например, для цикла программы СуммаЭлементовПоследовательности
ограничивающим может быть выражение
, а для программы НаибольшийОбщийДелитель--
выражение .
Следует признать, что некоторые циклы уже готовых программ чрезвычайно
трудны для понимания и могут потребовать больших интеллектуальных затрат
на поиск их инвариантов и ограничивающих выражений. Однако эти затраты
по существу и отражают реальную сложность, присутствующую в итеративных
программах. Поэтому программист должен проводить доказательство правильности
программы во время самого процесса программирования, причем находить инвариант
цикла и его ограничивающее выражение до, а не после того, как данный цикл
написан.
Next:4.1.3
Оператор цикла с условием на продолжение
Up:4.1
Средства для организации
Previous:4.1.1
Оператор цикла с условием на окончание