Инвариант цикла стратегии "максимум" на шаге I

max является максимумом из  :

Этот инвариант для n-го шага, случай I2 для i = n, дает

что и является желаемым результатом.

Следующая картинка иллюстрирует стратегию цикла для этого случая.

Рис. 7.6. Поиск максимума последовательными аппроксимациями

Цикл вначале устанавливает инвариант "max является максимумом первых i значений" для тривиального случая: i = 1. Затем повторно расширяется множество данных, на котором выполняется инвариант.

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

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

Стратегия цикла

Хотя большинство циклов более сложные, чем простой пример вычисления максимума, он иллюстрирует общую форму цикла как стратегию решения задач.

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

Чтобы использовать цикл, нужно найти слабую (более общую) форму цели Post: свойство INV (s) — инвариант цикла, определенный на подмножествах s из DS со следующими свойствами.

L1. Можно найти начальное подмножество Init из DS, такое, что начальное условие Pre влечет INV (Init ); другими словами, инвариант выполняется на начальном подмножестве.

L2. INV (DS) влечет Post (из истинности инварианта на всем множестве следует истинность цели).

L3. Известен способ, позволяющий расширить подмножество s, для которого инвариант INV(s) выполняется, на большее подмножество (s’) из DS, сохраняя при этом истинность инварианта.

Пример с максимумом имеет все три составляющие: DS — это множество чисел  ; предусловие Pre говорит, что DS имеет, по меньшей мере, один элемент; цель Post утверждает, что найден максимум этих чисел, а инвариант INV(s), где s — подмножество  , утверждает, что найден максимум на этом подмножестве. Тогда:

M1. Если Pre выполняется, (имеется хотя бы одно число), то нам известно начальное множество Init, такое, что INV (Init) выполняется. Для этого достаточно в качестве подмножества взять первый элемент  .

M2. INV (DS) — инвариант, применимый ко всему подмножеству  — влечет истинность цели, а фактически совпадает с целью Post.

M3. Когда INV(s) удовлетворяется на  , которое пока не совпадает со всем DS — другими словами, i < n, — то мы можем установить INV (s') для большего подмножестваs’ изDS: мы просто возьмем s' как  , а в качестве нового максимума большее из двух чисел: старого максимума и  . Заметьте: в общем случае нужно крайне тщательно проектировать инвариант, чтобы он позволял применить стратегию последовательной аппроксимации.

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

• Он достаточно силен, чтобы из него следовала цель Post, когда он выполняется на всем множестве.

• Он достаточно гибкий, чтобы позволять расширять множество, сохраняя его истинность.

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

Эти наблюдения определяют, как работает цикл в качестве структуры управления. Его выполнение проходит следующие этапы.

X1. Устанавливается INV (Init), используя преимуществ L1. Это дает нам Init как первое подмножество s, на котором выполняется INV.

X2. До тех пор, пока s не совпадает со всем множеством DS, применяется прием L3 для установления INV на новом, расширенном s.

X3. Останавливаемся сразу же, когда s совпадает с DS. В этот момент INVвыполняется на DS, что, благодаря L2, свидетельствует о достижении цели Post.

Этот процесс гарантирует завершаемость, поскольку мы предполагаем, что DS является конечным множеством, s всегда остается подмножеством DS и на каждом шаге увеличивается по крайней мере на один элемент, так что гарантируется, что после конечного числа шагов s совпадет с DS. В некоторых случаях, однако, установление завершаемости не столь просто.