Программирование не всегда начинается с проектирования, часто необходимо понять существующую программу, например для того чтобы модифицировать. Поскольку методы анализа программ, разработанные для 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 --> F
= (Y <= 0 --> (Y >= 0 --> X, Y:= X+Y, 0) | (Y <= 0 --> (Y < 0 -->))
= (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.
Композиция F с первыми присваиваниями
(X, Y:= 3, 5) ◦ F
дает значение всего фрагмента программы:
(5 > 0 --> X, Y:= 3 + 5, 0) | (5 <= 0 --> X, Y:= 3, 5) =
(X, Y:= 8, 0)
Желаемая функция для оператора 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, выполняются аналогично предыдущему примеру.