Одсчет итераций для операторов WHILE

8. ИСЧИСЛЕНИЕ ЦИКЛИЧЕСКИХ ВЫРАЖЕНИЙ.

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

Значение программы, не содержащей итераций, может быть вычислено напрямую, за один шаг. Сначала вычисляется значение (символьных, файловых, логических) выражений, далее операторов присвоения, READ, WRITE, BEGIN, декларации, блоки, заголовок и завершающая точка программы. В любом случае частное значение определяется через текст соответствующей части программы. Для итераций, тексты условия WHILE и выражения DO могут быть использованы много раз, поэтому определение значения является более сложным.

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

начение циклов.

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

Значение оператора WHILE может быть определено напрямую из способа каким оно выполняется. Пусть w будет:

WHILE b DO d

где b – логическое выражение, а d – оператор. В состоянии выполнения, где b имеет значение T, d выполняется, возможно, изменяя состояние, и далее w выполняется снова, с новым состоянием. Если b имеет значение F для какого-то состояния, тогда w выполняется аналогично пустому оператору на этом состоянии. Поведение w может быть описано через оператор IF:

IF b THEN BEGIN d; w END

Тогда формальное определение будет:

w = IF b THEN BEGIN d; w END

Простые операторы WHILE могут быть проанализированы напрямую, например, пусть v будет:

WHILE V1 < V2 DO V1 := V2

По определению:

v = IF V1 < V2 THEN BEGIN V1 := V2; v END

Поскольку v в правой части (внутри BEGIN … END) будет всегда применяться к состоянию, где было только что выполнено присваивание V1 := V2, логическое выражение V1 < V2 в всегда будет F. Поэтому v в правой части может быть удалено, поскольку в данном случае но выполняет те же действия что и пустой оператор. Таким обрахзом,

v = IF V1 < V2 THEN V1 := V2

Значение v теперь стало более легким для понимания, поскольку мы устранили итерацию.

Второй пример, пусть u будет:

WHILE V1 <= V2 DO V1 := V2

Здесь u отличается от v только оператором сравнения в условии цикла. Небольшое изменение ведет к радикальному изменению поведения. По определению:

u = IF V1 <= V2 THEN BEGIN V1 := V2; u END

Как и для v, состояние, в котором выполняется повторение u, благодаря присваиванию, имеет одинаковые значения для V1 и V2. Логическое условие для u всегда T для такого состояния, поэтому для любого начального состояния, где условие цикла имеет значение T, мы попадаем в ситуацию бесконечного выполнения, т.е. ошибки времени выполнения, значение оператора здесь не определено. Для любого другого состояния значением u является функция эквивалентности (выполняется пустой оператор).

u = {<s, s>: V1 <= V2 (s) = F}

Рассмотрим более сложный пример. Пусть t ,будет:

WHILE V1 < V2

BEGIN

V1 := V2;

V2 := V3

END

Часть DO может быть представлена одновременным присваиванием:

V1, V2 := V2, V3

Если часть DO, будет повторно выполнена несколько раз, значения переменных будут следующими:

	V1	V2
V1, V2 := V2, V3	V2	V3
V1, V2 := V2, V3	V3	V3
V1, V2 := V2, V3	V3	V3

То есть после второй итерации содержат значение, которое изначально было в V3 и после этого уже ничего не меняется. Эта таблица позволяет легкий способ проанализировать t. Условие завершения цикла V1 >= V2 и из таблицы видно, что это случается не более чем через две итерации. Вторая итерация случается только тогда, когда начальное значение V2 не предшествует начальному значению V3, потому что это значения V1 и V2 соответственно, после первой итерации. Эта информация обобщается условным присваиванием, выражающим значение t.

(V1 >= V2 -> ) | (V2 >= V3 -> V1, V2 := V2, V3) | (V1, V2 := V3, V3)

Первый элемент выражения описывает случай, когда итерация не выполняется, второй – когда выполняется одна итерация, третий – две итерации.

Запишем полных защитников для каждого элемента:

(V1 >= V2 -> ) | (V1 < V2 -> (V2 >= V3 -> V1, V2 := V2, V3))

| (V1 < V2 -> (V2 < V3 -> V1, V2 := V3, V3))

одсчет итераций для операторов WHILE

В таблице выполнения выполнение оператора WHILE отображается повторением оператора в части DO. Повторение продолжается, пока не выполнится условие завершения цикла. Когда количество повторений может быть определено, это позволяет нам получить другой способ понимания значения оператора WHILE.

Пусть w будет

WHILE b DO d

где b – логическое выражение, а d – оператор. Domain(w) – это набор состояний выполнения для которых выполнение w может быть завершено. Для каждого состояния s Î domain(w) число итераций может быть целым числом k. (В противном случае будет бесконечное выполнение для состояния s, которое не в domain(w)).

Например, в операторе WHILE, рассмотренном выше, k было 0, 1 или 2. Несколько фактов о w и начальном состоянии s могут быть получены из k.

Если k = 0, тогда b(s) = F, иначе выполнилась хотя бы одна итерация. w(s) = s поскольку d не выполнялось.

Если k =1, тогда

b(s) = T

w(s) = d(s)

(d◦b)(s) = F

Первое условие необходимо для любого количества итераций. Второе выражение отражает эффект от ровно одного выполнения d. Третье выражение объясняет, почему не произошла вторая итерация. После того как часть DO была выполнена, новое состояние d(s) ведет к невыполнению условия b:

b ((d)(s)) = (d◦b)(s) = F

Если k = 2, тогда

b(s) = T

(d◦b)(s) = T

w(s) = d(s)◦ d(s)

(d◦d◦b)(s) = F

Здесь первые два вычисления b позволяют циклу выполняться, часть DO d будет выполнена дважды, и третье вычисление b должно вызвать прекращение цикла.

Общий механизм достаточно прозрачен и он может быть выражен в общем виде для k >= 0 итераций оператора w в состоянии s Î domain(w):

(d⁰◦b)(s) = T

(d¹◦b)(s) = T

…

(d^k-1◦b)(s) = T

w(s) = d^k(s)

(d^k◦b)(s) = F

Число в индексе означает многократную композицию d. Для любого отношения r

r⁰ = {<x, x>: x Î domain(r)}

rⁿ = r ◦ rⁿ^-1, n > 0

Специальный случай нуля композиций r, записываемый r⁰, определен как функция эквивалентности I. Используется как определение нуля итераций оператора WHILE.

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

V1 < V2 (s) = T

V1 := V2; V2 := V1¹ ◦ V1 < V2 (s) = T

t(s) = V1 := V2; V2 := V1²(s), V1 := V2; V2 := V1² ◦ V1 < V2 (s) = F

Удобство и мощь рассмотренного подхода позволяет нам заключить, что во многих случаях количество итерации является эффективным способом для разметки domain(w) в целях изучения и анализа.

Например, выражение WHILE для поглощения пробелов будет выполнено столько раз, каково количество пробелов в строке будущего файла.

Итеративное определение оператора WHILE может быть дано в следующем виде:

WHILE b Do d =

{

<s, t>: для некоторого целого числа k выполняются следующие условия:

1. t = d^k (s)

2. для любого целого числа i меньшего k, (dⁱ◦b)(s) = T

3. b(t) = F

}

Это определение эквивалентно следующему рекурсивному, которое может быть получено, если рассматривать варианты для k = 0, 1, 2, …

WHILE b DO d = IF b THEN BEGIN d; WHILE b Do d END

Его мы и будем использовать.

Оператор WHILE может быть проанализирован рассмотрением условия завершения для каждого s Î domain(w) для нахождения количества итераций k. Значение в таком случае будет композицией k значений части DO.

Например, рассмотрим оператор WHILE:

WHILE V1 < V2

BEGIN

V1 := V3;

V3 := V2;

V2 := V4

END

Часть DO имеет значение одновременного присваивания:

V1, V2, V3 := V3, V4, V2

Три итерации этого значения показаны в трассировочной таблице:

	V1	V2	V3
V1, V2, V3 := V3, V4, V2 V1, V2, V3 := V3, V4, V2 V1, V2, V3 := V3, V4, V2	V3 V2 V4	V4 V4 V4	V2 V4 V4

Из таблицы можно увидеть, что условие прекращения в терминах начальных значений будет следующим:

Итерация	Условие
	V1 >= V2 V3 >= V4 V2 >= V4 V4 >= V4

Таким образом, здесь может быть не более трех итераций, поскольку условие прекращения всегда истинно после третьей. Из этих двух таблиц может быть получено значение оператора в виде условных присваиваний, руководствуясь количеством итераций и одновременными присваиваниями из трассировочной таблицы.

(V1 >= V2 -> ) | (V3 >= V4 -> V1, V2, V3 := V3, V4, V2) |

(V2 >= V4 - > V1, V2, V3 := V2, V4, V4) | (V1, V2, V3 := V4, V4, V4)

В качестве другого примера рассмотрим оператор WHILE, поглощающий пробелы из INPUT:

WHILE (Ch = ‘ ’) AND NOT EOF

READ(Ch)

Предположим, что начальное состояние выполнения будет s = {Ch·N, INPUT·<x, y. R>, …},

Тогда выражение Ch = ‘ ’будет равно F и оператор WHILE будет выполнен ноль раз.

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

((Ch = ‘ ‘) AND (INPUT = <x, y, R>) -> Ch, INPUT := c, <x & u Ñ c, v, R>) |

((Ch <> ‘ ‘) OR (INPUT = <x, ††, R>) -> )

где

y = u Ñ C & k, и