Программирование не всегда начинается с проектирования, часто необходимо понять существующую программу, например для того чтобы модифицировать. Поскольку методы анализа программ, разработанные для CF Pascal зависят только от определения box-функций, они могут быть применены для дополнительных типов данных, таких как INTEGER. Рассмотрим следующий фрагмент программы.
BEGIN
X := 3;
Y := 5;
{(Y >= 0 --> X, Y := X+Y, 0) | (Y < 0 --> )}
WHILE Y > 0
DO
BEGIN
Y := Y – 1;
X := X + 1
END
END
Желаемая функция для оператора WHILE представлена комментарием:
F = (Y >= 0 --> X, Y := X+Y, 0) | (Y < 0 --> )
Правило верификации для WHILE требует выполнения следующих трех условий:
1. domain(F) = domain( WHILE Y > 0 DO BEGIN Y := Y – 1; X := X + 1 END )
2. (Y <= 0 -> F) = (Y <= 0 -> )
3. F = IF Y > 0 THEN BEGIN Y := Y-1; X := X + 1 END
Область определения F все состояния, поэтому завершение требуется для всех значений Y. Если значение Y отрицательное или ноль, оператор WHILE пропускается, поэтому завершение гарантировано. Если значение Y положительное, оператор WHILE выполняется и Y уменьшается, и окончательное завершение гарантируется, поскольку значение Y приближается к нулю. Таким образом, первое условие удовлетворяется.
Мы можем переписать левую сторону второго условия так что она будет идентичная правой части.
= (Y <= 0 AND Y >= 0 --> X, Y := X+Y, 0) | (Y <= 0 AND Y < 0 --> )
= (Y = 0 --> X, Y := X+Y, 0) | (Y < 0 --> )
= (Y <= 0 --> )
Наконец, рассмотрим правую часть третьего условия:
IF Y > 0 THEN BEGIN Y := Y-1; X := X + 1 END ◦ F
Функция, соответствующая оператору IF будет:
IF Y > 0 THEN … = (Y > 0 -- > X, Y := X + 1, Y - 1) | (Y <= 0 --> )
тогда IF Y > 0 THEN … ◦ F будет
(Y > 0 -- > X, Y := X + 1, Y - 1) | (Y <= 0 --> ) ◦
(Y >= 0 --> X, Y := X+Y, 0) | (Y < 0 --> )
Здесь необходимо рассмотреть четыре случая соответствующих первому и второму условиям двух условных присваиваний. Обозначим эти случаи по номеру выбранного условия, например, случай 1-2 будет означать первое условие IF Y > 0 THEN … и второе условие F:
Случай 1-1
Часть
Условие
X
Y
IF …
F
Y > 0
Y – 1 >= 0
X + 1
X + 1 + Y - 1
Y – 1
Условие упрощается до Y >= 1, тогда функция будет:
(Y >= 1 --> X, Y := X + Y, 0)
Случай 1-2
Часть
Условие
X
Y
IF …
F
Y > 0
Y – 1 < 0
X + 1
Y – 1
Условие:
Y > 0 AND Y – 1 < 0 = Y > 0 AND Y < 1
не может быть удовлетворено, поэтому этот случай не произойдет.
Случай 2-1
Часть
Условие
X
Y
IF …
F
Y <= 0
Y >= 0
X + Y
Условие упрощается до Y = 0, тогда функция будет:
(Y = 0 --> )
Случай 2-2
Часть
Условие
X
Y
IF …
F
Y <= 0
Y < 0
Условие:
(Y < 0 --> )
Собирая функцию из четырех частей вместе, получим:
(Y >= 1 --> X, Y := X + Y, 0) | (Y = 0 --> ) | (Y < 0 --> )
= (Y > 0 --> X, Y := X + Y, 0) | (Y <= 0 --> )
Таким образом, правая сторона третьего условия идентична F, что и требовалось доказать.
Поскольку условия верификации оператора WHILE удовлетворены, F – функция вычисляемая оператором WHILE.
Желаемая функция для оператора WHILE не всегда дается как условное присваивание, часто желаемая функция должна быть получена из программы. В предыдущем примере было легко определить функцию для оператора WHILE, потому что оба оператора присваивания в ней были накапливающими операторами присваивания. В накапливающем присваивании значение переменной изменяется прибавлением или вычитанием фиксированного значения. Математическая концепция суммирования (повторяющегося сложения) – естественный выбор для описания повторяющиеся эффекты для X и Y. Поскольку цикл выполняется так долго, как Y > 0 и значение Y уменьшается на 1 в течение каждого выполнения, суммирование будет содержать Y элементов. На каждой итерации, поскольку X и Y изменяются на константу 1, это элемент для суммирования. Сумма добавляется к исходному значению X и вычитается из исходного значения Y. Таким образом функция для оператора WHILE будет:
X, Y := X + ,
Эти значения могут быть упрощены:
X + = X + (Y –1 + 1) = X + Y – 1 + 1 = X + Y
= Y – 1(Y – 1 + 1) = Y – Y – 1 + 1 = 0
то есть функция будет:
(X, Y := X+Y, 0)
как и ранее.
Этот метод может быть использован для определения функции другого оператора WHILE. Фрагмент на Паскале ниже эмулирует операторы DIV и MOD используя только сложение и вычитание. Его желаемая функция будет:
f = (Numerator >= 0 AND Denominator > 0 -->
Quotient, Remainder :=
Numerator DIV Denominator, Numerator MOD Deniminator)
Для данной функции фрагмента программы должна быть определена функция вычисляемая оператором WHILE для того, чтобы верифицировать, что фрагмент вычисляет f.
Quotient := 0;
Reminder := Numerator;
WHILE Remider >= Denominator
DO
BEGIN
Quotient := Quotient + 1;
Reminder := Reminder - Denominator
END
Пусть значения Quotinet, Reminder и Denominator будут Q, R и D соответственно. Тест на завершение будет R ≥ D или R- D ≥ 0, цикл будет выполнен k раз, где:
k = (R-D) / D = R/D –1
Таким образом, Q и R изменяться до:
Q +
R -
соответственно. Эти выражение сокращаются до:
Q + = Q + 1 (R / D)
R - = R – D(R/D)
Функция для оператора WHILE следующая:
(Reminder >= Denominator AND Denominator > 0 -->
Remainder, Quotient :=
Reminder – (Reminder DIV Denominator)*Denominator,
Quotient + (Reminder DIV Denominator)) |
(Reminder < Denominator --> )
Верификация, что это функция оператора WHILE и фрагмент программы корректен для данной желаемой функции f, выполняются аналогично предыдущему примеру.
, 
