Правило верификации рекурсивных процедур

Также как не всегда возможно раскрывать операторы WHILE пока они не завершатся, или увидеть общий случай так, чтобы можно было подсчитать количество итераций, так и не всегда возможно развернуть рекурсию. Может так случиться, что выражения, управляющие рекурсией слишком сложны для анализа и требуются другие методы. Для операторов WHILE было достаточно развернуть цикл однажды и получить рекурсивное уравнение. Для рекурсивных процедур такое уравнение может быть получено напрямую. В программе существуют как минимум два процедурных оператора: исходный оператор вызова процедур и рекурсивный вызов.

Вычисляем значение процедурного оператора в операторе BEGIN процедуры LengthOfInput:

Count = BEGIN IF NOT EOLN THEN …

= {< s, t>: EOLN(s) = TRUE, t = Number: = ‘0’ (s)}

È {< s, t>: EOLN(s) = FALSE, t = (READ(Nc)·Count·NextDigit(Number))(s)}

Функция Count присутствует явно в левой и правой частях этого рекурсивного уравнения. В общем случае решение такого уравнения очень сложно, но гораздо легче протестировать определенную функцию, чтобы посмотреть есть ли решение.

Если верить тому, что мы написали в комментарии LengthOfInput, значение Count – функция f, определяемая условным присваиванием

(EOLN -> Number: = ‘0’) | (NOT(EOLN) -> Number, Nc: = m mod 10, c)

где m – длина строки будущего INPUT до следующего конца строки, а c – последний символ перед маркером конца строки.

Заменяя Count на f в рекурсивном уравнении, рассмотрим два варианта, с пустой и непустой строкой будущего L, до первого символа конца строки.

Вариант 1. L пуста. Тогда для состояния s, левая часть рекурсивного уравнения в f, будет

f(s) = t, где t такое же как s, за исключением того, что значение Number - символ, представляющий 0 mod 10, т.е. 0

Правая часть первым множеством, где EOLN(s) = TRUE и в этом множестве s образует пару с таким же t. То есть в случае 1 f удовлетворяет рекурсивному уравнению.

Вариант 2. L не пуста. Пусть длина L будет k > 0, а последний символ с. Тогда для состояния s левая часть рекурсивного уравнения в f будет

f(s) = t, где t такое же как s за исключением того, что значение Number - символ, представляющий k mod 10 а значение Nc – с.

Правая часть покрывается вторым множеством, где EOLN(s) = TRUE и в значение, образующее пару с s, будет

t = (READ(Nc)·Count·NextDigit(Number))(s)

t может быть вычислено с помощью таблиц трассировки

Вариант 2.1.

Условие: (LÑ / ¹ ††) AND (Θ (Λ (LÑ /)) = /)

Присваивание: Number, Nc: = ‘1’, c

Условие выполняется только когда L – 1-строка, а поскольку L – 1-строка, Θ (LÑ /) = c, потому что он единственный символ в L (до маркера конца строки).

Таким образом, не учитывая происходящее с INPUT, условное присваивание будет

(длина(L) = 1 -> Number, Nc: = ‘1’, c)

Вариант 2.2.

NextDigit увеличивает Number за исключением значения 9, которое становится 0. Это поведение описывается добавлением функции mod 10 – остаток от деления на 10.

Условие: (LÑ / ¹ ††) AND (Θ (Λ (LÑ /)) ¹ /)

Присваивание: Number, Nc: = (длина(Λ (LÑ /)) mod 10 + 1) mod 10, c

Условие может быть упрощено наблюдением, что L должна быть как минимум 2-строкой, потому что Λ (L) не должен начинаться с маркера конца строки.

Таким образом, не учитывая происходящее с INPUT, условное присваивание будет

(длина(L) > 1 -> Number, Nc: = (длина(Λ (LÑ /)) mod 10 + 1) mod 10, c)

Отметим, что

длина(Λ (LÑ /)) mod 10 + 1 = длина(LÑ /) mod 10

для всех длина (L) > = 1 и применение второй функции mod не дает эффекта.

Случай 2.1 и 2.2 могут быть объединены:

(длина(L) > = 1 -> Number, Nc: = длина(Λ (LÑ /)) mod 10, c)

Это точно то, что было получено для левой части, таким образом, f удовлетворяет рекурсивному уравнению в случае 2. Было показано, что функция f построенная из комментария в LengthOfInput, удовлетворяет рекурсивному уравнению для Count в данной программе.

Однако, как и в случае с оператором WHILE, требуется осторожность, поскольку рекурсивное уравнение не единственное необходимое условие. Может случится, что функция удовлетворяет рекурсивному уравнению, но не является значением процедуры, из которой было выведено это уравнение.

Например, процедура

PROCEDURE Forever;

BEGIN

Forever

END;

чье рекурсивное уравнение будет

Forever = Forever

и любая функция, какую бы мы не взяли, будет решением. Для этой процедуры значением должна быть пустая функция, поскольку рекурсия никогда не завершается.

По аналогии со случаем для оператора WHILE, это предлагает правило верификации: функция частного значения для процедурного оператора, включающего рекурсивный вызов это решение рекурсивного уравнения, область определения которого согласуется с областью определения процедуры.

Пусть P будет процедурный оператор для процедуры без параметров с одним рекурсивным вызовом, имеющим рекурсивное уравнение P = M(P). M(P) представляет результат вычисления функции частного значения < блока> процедуры, в котором P встречается только один раз. Вычисление должно производиться до тех пор, пока явно не встретится P как в примере выше. Функция f = P если и только если:

1. domain(f) = domain(P), и

2. f является решением рекурсивного уравнения.