Правила проектирования.
Правила проектирования для операторов BEGIN, IF и WHILE в CF Pascal могут быть расширены для D Pascal и его перечислимых типов. Единственное требуемое изменение – это правило сохранности для операторов BEGIN:
Для CF Pascal оно будет:
На каждом шаге сохраняйте все исходные значения правой части запланированного одновременного присваивания.
Слово «сохраняйте» может быть заменено на «сохраняйте возможность вычисления», то есть:
На каждом шаге сохраняйте возможность вычисления всех исходных значений правой части запланированного одновременного присваивания.
Поскольку арифметические операции имеют противоположные операции, то удовлетворение новому правилу обеспечения сохранности не всегда требует временных переменных.
Рассмотрим задачу построения оператора BEGIN для обмена двух целых значений без использования временной переменной.
X, Y := Y, X
Хотя временная переменная потребуется, чтобы сохранить значение X или Y перед тем как оно будет, одно значение и сумма этих двух значений сохраняют возможность вычислить оба, поскольку одно значение может быть вычтено из суммы для получения другого. То есть следующий подход приемлем:
BEGIN
X := X + Y;
Y := X – Y;
X := X – Y;
END:
Значения X и Y, конечно, должны лежать в интервале [-MAXINT, MAXINT], но обмен не будет работать, как требуется для всех этих значений. Результат каждой операции может также не попасть в интервал. Условия корректного выполнения вычислены в следующем символическом выполнении. Аббревиатура inrange(X) означает, что значение X находится в интервале [-MAXINT, MAXINT].
| Часть | Условие | X | Y |
| X := X + Y Y := X – Y X := X - Y | inrange(X+Y) inrange(X+Y-Y) inrange(X+Y-X) | X X+Y X+Y-X=X | Y X+Y-Y=X |
Легко видеть, что все условия очевидно выполнимы, если выполнимо первое. Таким образом, функция, вычислимая данным кодом будет:
(inrange(X+Y) -> X,Y := Y, X)
Переполнение не часто требует такой формальности, но проблема существует всегда.
Как другой пример проектирования с использованием типа INTEGER, рассмотрим моделирование сложения циклическим прибавлением единицы. То есть для сложения значений X и Y спроектируем оператор WHILE для добавления единицы Y раз к X.
Переполнение с этого момента мы отслеживать не будем, тогда требуемая функция будет:
f= (0 <= Y -> X := X+Y)
Существование условия правила проектирования операторов WHILE требует, чтобы
range(f) Í domain(f)
и это условие удовлетворено и
для каждого s Î range(f), f(s) = s.
Последнее условие не срабатывает. Рассмотрим состояние s в range(f), в котором значение Y ненулевое. f ставит в соответствие этому состоянию состояние, в котором значение X заменяется значением X+Y, которое отличается от X, поэтому новое состояние не может быть s, как требует условие существования.
Возможно, оператор WHILE не может быть разработан, если значение Y можно будет менять, но тот же аргумент показывает, что вторая часть условия существования не будет срабатывать до тех пор пока новое значение Y не будет нулем. Таким образом, рассмотрим:
g=(0<=Y -> X,Y := X+Y, 0)
как целевую функцию. range(s) – те состояния, в которых значение Y равно нулю и определено на всех таких состояниях, поэтому условие:
range(g) Í domain(g)
удовлетворяется. Так же удовлетворяется вторая часть условия существования,
g(s) = s для всех s Î range(g)
потому что любое состояние s Î range(g) имеет нулевое значение Y и g добавляет нуль к X, оставляя его неизменным.
С удовлетворенным условием существования, условие WHILE B должно быть выбрано так что:
B(s) является TRUE для всех s Î domain(g) - range(g),
B(s) является FALSE для всех s Î range(g),
В domain(g) значение Y неотрицательное и поскольку значение Y нулевое в range(g), простейшее выражение для B будет Y > 0.
Наконец, оператор BEGIN D, должен быть выбран такой, что
WHILE Y > 0 DO D
завершается для любого состояния в domain(g) и
IF Y > 0 THEN D
сохраняет значения необходимые для достижения финального состояния, то есть X+Y.
Для завершения цикла Y может уменьшаться на единицу на каждом шаге. Таким образом, оператор WHILE, спроектированный для g будет:
WHILE Y > 0
DO
BEGIN
Y := Y –1;
X := X+1
END