Анализ программ.

Программирование не всегда начинается с проектирования, часто необходимо понять существующую программу, например для того чтобы модифицировать. Поскольку методы анализа программ, разработанные для 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

Условие упрощается до Y > = 1, тогда функция будет:

(Y > = 1 --> X, Y: = X + Y, 0)

Случай 1-2

Условие:

Y > 0 AND Y – 1 < 0 = Y > 0 AND Y < 1

не может быть удовлетворено, поэтому этот случай не произойдет.

Случай 2-1

Условие упрощается до Y = 0, тогда функция будет:

(Y = 0 -->)

Случай 2-2

Условие:

(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, выполняются аналогично предыдущему примеру.

Заключение.

В этой главе были рассмотрены порядковые типы данных Паскаля. Операции, которые могут быть применены к каждому типу, обобщены в следующей таблице.

Каждый порядковый тип используется по-своему. Переменные типа BOOLEAN могут быть использованы для хранения сложных условий для дальнейшего использования. Переменные типа INTEGER позволяют легко выполнять подсчет при условии, что выполняется ограничение [-MAXINT, MAXINT]. Перечислимые типы хороши, когда нужно зафиксировать небольшой набор значений, каждое со своим мнемоническим именем. Типы диапазоны позволяют программисту объявлять границы их значений, чтобы они проверялись автоматически.

Методы анализа, использованные в CF Pascal, расширены до использования с порядковыми типами без изменений.