С каждой точкой разреза k свяжем предикат
invk (x1, …, xn),
который будем называть индуктивным утверждением. Назначение этого предиката состоит в том, чтобы описать соотношение между переменными в этой точке. Всякий раз, когда исполнение программы достигает точки k, предикат invk (x1, …, xn) должен быть истинным для текущих значений x1, …, xn в этой точке.
Индуктивное утверждение, приписанное циклу, принято называть инвариантом цикла. Инвариант цикла может приписываться точке входа в цикл или любой другой точке цикла, которая лежит на каждой трассе через цикл.
Будем считать, что программа аннотируется выбором контрольных точек (на входе программы, выходе программы и на каждом пути через цикл), с каждой из которых связывается индуктивное утверждение (инвариант):
invt1 (x1, …, xn): P; invt2 (x1, …, xn): Q; invt3 (x1, …, xn); …,
где t1 – точка входа (после оператора START), t2 – точка выхода (перед оператором STOP), t3 – контрольнаяточка инварианта цикла.
Шаг 3. Определение набора условий корректности для всех путей между соседними контрольными точками программы
|
|
Пусть путь a ведет от контрольной точки r к контрольной точке t (случай r = t не исключается) и не содержит никаких других контрольных точек и пусть этот путь проходит черезпоследовательность операторов A1, A2, …, Ai,, …, Ak, где Ai – оператор присваивания или условие re, где e Î { +, - }.
Определим условие Ua пути a между двумя соседними контрольными точками графа потока управления программы следующим образом:
Ua: invr(x1, …, xn) Þ U0
(из истинности предиката в начальной контрольной точке r следует истинность условия U0), где последовательность U0, U1, …, Uk задается по индукции (методом обратной подстановки):
1. Uk: invt (x1, …, xn) – условие определяется предикатом в контрольной точке t;
2. Пусть Ui определено. Тогда возможны два случая:
a) Ai – оператор присваивания xs:= f (x1, …, xn), тогда
Ui-1: Ui (xs f (x1, …, xn));
b) Ai – условный оператор re, тогда
Ui-1: r Þ Ui при e = + или
Ui-1: Ør Þ Ui при e = –
Пример
Пусть a соответствует последовательности:
x = f1 (x); g+ (x); x = f2 (x); h– (x); x = f3 (x);
Тогда
P: invr (x) – входной предикат;
U5 : Q = invt (x);
U4 : Q (f3 (x));
U3 : (Ø h (x) Þ Q (f3 (x)));
U2 : (Ø h (f2 (x)) Þ Q (f3 (f2 (x))));
U1: (g (x) Þ (Ø h (f2 (x)) Þ Q (f3 (f2 (x))));
U0: (g (f1 (x)) Þ (Ø h (f2 (f1 (x))) Þ Q (f3 (f2 (f1 (x))));
Окончательно условие пути a имеет вид:
Ua: P Þ (g (f1 (x)) Þ (Ø h (f2 (f1 (x))) Þ Q (f3 (f2 (f1 (x))));