Схема проектирования цикла

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

цикла,
но и для его проектирования в процессе разработки программы.

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

while с заданной спецификацией (P, Q) :
{P} S0;  while (B) S;

{Q},
где S – тело цикла, S0 – операторы инициализации цикла, а предикат B в соответствии с семантикой цикла while есть условие продолжения цикла.
Пусть X – множество переменных программы, X0 – их начальные значения, установленные действием S0.
Не ограничивая общности, представим тело цикла в виде X = f(X), где f – функция, описывающая преобразование переменных в теле цикла S.

false}; т. е. P – предикат, выражающий предусловие;
Q: M →  Boolean, т. е. Q – предикат,

выражающий постусловие.
Кроме того, обозначим множества:
P = {X ∈ M : P(X) = true};
Q = {X ∈ M : Q(X) = true};
B = {X ∈ M : B(X) = true};
B * = {X ∈ M : B(X) = false}.
Рассмотрим предикат inv : M →  Boolean и множество I = {X ∈ M : inv (X) = true}. Кроме того, введем некоторую целочисленную функцию переменных программы t: I → N0, где N0 – множество неотрицательных целых чисел.

что справедливы следующие утверждения:
inv & !B → Q;
{P} S0 {inv}
{inv & B } S {inv};
inv (X) & B(X) → (t(X) > 0);
{inv (X) & B(X) & t0 = t(X)} S {0 ≤ t(X) 

while завершается и имеет «заявленное» свойство {P} S0;  while (B) S; {Q}.
Интерпретация этого факта в терминах преобразования f переменных в теле цикла:
свойство {inv & B } S {inv} тела цикла детализируется как {inv (X) & B(X) } X = f(X) {inv(X)},
и по правилу вывода для оператора присваивания имеем inv (X) & B(X) → inv(f(X)),
т.е. преобразование f на множестве I ∩ B  сохраняет инвариант inv.

: Q(X) = true};
B * = {X ∈ M : B(X) = false}.
I = {X ∈ M : inv (X) = true}

inv (X)  & not B (X)  → Q (X)

более чем t (X0) гарантировано приведет к достижению в множестве M

точки X ∈ I ∩ B *  и при этом  I ∩ B * ⊂ Q , т. е. X ∈ Q и следовательно Q(X) = true.

цикла с заданными пост- и предутверждениями состоит в следующем.
Начинают с

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

Затем надо:
сформулировать условие продолжения цикла B (или завершения !B);
попытаться придумать инвариант цикла inv и вариант var.
Если это удалось, то набросок цикла можно записать в виде:

}
Фрагмент Б
//Постусловие: Q
После этих действий остается:
обеспечить при заданном предусловии выполнение

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