Шаг 2. Получение аннотированной программы

С каждой точкой разреза k свяжем предикат

inv_k (x₁, …, x_n),

который будем называть индуктивным утверждением. Назначение этого предиката состоит в том, чтобы описать соотношение между переменными в этой точке. Всякий раз, когда исполнение программы достигает точки k, предикат inv_k (x₁, …, x_n) должен быть истинным для текущих значений x₁, …, x_n в этой точке.

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

Будем считать, что программа аннотируется выбором контрольных точек (на входе программы, выходе программы и на каждом пути через цикл), с каждой из которых связывается индуктивное утверждение (инвариант):

inv_t₁(x₁, …, x_n): P; inv_t₂(x₁, …, x_n): Q; inv_t₃(x₁, …, x_n); …,

где t1 – точка входа (после оператора START), t2 – точка выхода (перед оператором STOP), t3 – контрольнаяточка инварианта цикла.

Шаг 3. Определение набора условий корректности для всех путей между соседними контрольными точками программы

Пусть путь a ведет от контрольной точки r к контрольной точке t (случай r = t не исключается) и не содержит никаких других контрольных точек и пусть этот путь проходит черезпоследовательность операторов A₁, A₂, …, A_i_,, …, A_k, где A_i – оператор присваивания или условие r_e, где e Î { +, - }.

Определим условие U_a пути a между двумя соседними контрольными точками графа потока управления программы следующим образом:

U_a: inv_r(x₁, …, x_n) Þ U₀

(из истинности предиката в начальной контрольной точке r следует истинность условия U₀), где последовательность U₀, U₁, …, U_k задается по индукции (методом обратной подстановки):

1. U_k: inv_t (x₁, …, x_n) – условие определяется предикатом в контрольной точке t;

2. Пусть U_i определено. Тогда возможны два случая:

a) A_i – оператор присваивания x_s:= f (x₁, …, x_n), тогда

U_i_-1: U_i (x_s f (x₁, …, x_n));

b) A_i – условный оператор r_e, тогда

U_i-1: r Þ U_i при e = + или

U_i-1: Ør Þ U_i при e = –

Пример

Пусть a соответствует последовательности:

x = f₁(x); g₊(x); x = f₂(x); h_–(x); x = f₃(x);

Тогда

P: inv_r (x) – входной предикат;