GNU C: Рекуррентный цикл и инвариантность в нем данных
Что это такое
Алгоритм цикла, оперирующий с одной и той же последовательностью данных, должен быть инвариантен, т.е отвечать условию изменения их значений на каждом проходе к некоторой константе и/или порождающему её утверждению, а так же сохранять истинность до своего начала и при выходе из него.
1. Утверждения
1.1 Инвариантность алгоритма цикла (далее – цикл), как и сам инвариант, имеют право на существование тогда и только тогда, когда цикл оперирует с одними и теми же переменными, являющиеся рекуррентным, т.е. изменяют свое состояние от предыдущего к последующему.
(п.2.1 настоящего документа)
1.2 Любой оперирующий с одними и теми же переменными циклический алгоритм должен быть проверен с использованием инварианта не только после входа в него, но и до момента использования, т.е. на начальном этапе – инициализации переменных цикла.
(п.2.2 настоящего документа)
1.3 Цикл должен быть инвариантен на всех своих проходах после входа в него.
(п.2.3 настоящего документа)
1.4 Цикл должен быть инвариантен в момент выхода из него и после его завершения.
(п.2.4 настоящего документа)
2. Доказательство
Для этого в алгоритм цикла вводится инвариант цикла, который является логическим выражением и сохраняет "истинность", неизменяя свое утверждением на каждой новой итерации, начиная с первой после входа в него.
2.1. Доказательство инвариантности цикла
Пусть существует некоторый алгоритм цикла, состоящий из последовательности команд, которые представляют собой выражение (у математиков – функция) $F(X_k)$, содержащее как минимум один оператор и одну, две и более переменных, значения которых изменяются от одного прохода цикла к другому. Поэтому проверке подлежат соотношение состояний всех задействованных в цикле переменных из общего набора $X_k=(x_k,y_k,...,z_k)$, которые изменяют свое состояние на каждой $k-ой$ итерации или прохода выполнения цикла. При этом, выражение $F(X_k)$ должно быть истинно на всем протяжении выполнения цикла.
(продолжение доказательства рекуррентности цикла в п.2.3)
2.2. Цикл должен быть инвариантен до первого прохода
Состояние всех переменных цикла $X_k$ должно быть инвариантно начиная с момента инициализации цикла, а не входа в него. Таким образом, инвариант $I(X_0)$ должен возвращать истинное состояние всех переменных $X_0$ перед началом выполнения цикла, а не после входа в него. Следовательно:
$I(X_0) \Rightarrow G(X_0)$(1)
Данная проверка вытекает из-за того, что на нулевой итерации, предваряющей выполнение цикла, решается вопрос: "входить в него или нет?"
Поэтому, кроме условия инвариантности цикла, должна проводиться одновременно проверка на истинность достяжения им целевого назначения $G(X_0)$, т.е. условие выполнения цикла наступило и "истинно" или не наступило, т.е. "ложно". Если оно наступило и истинно, входить в цикл не имеет смысла. В обратном случае, побежали дальше.
При этом вне зависимости оттого бежим мы или не бежим, инвариант $I(X_0)$ будет всегда "истинным", в то время как целевое условие $G(X_0)$ может быть как "истинным" (бежим), так и "ложным" (не бежим).
2.3. Цикл должен быть инвариантен на всех своих проходах
После выполнения входа в цикл и до конца первого прохода выражением $F(X_{k-1})$ переменным будут присвоены новые значения из общего набора $X_k$ :
$X_k \leftarrow F(X_{k-1})$(2)
Затем, выполняется проверка на соблюдение условий инвариантности и целевого назначения цикла по формуле (1), только с одним изменением, что счетчик итераций цикла $к-й$ принимает значения $1,2,3,...,N$:
$I(X_k) \Rightarrow G(X_k)$(3)
Таким образом, мы имеем дело с рекуррентным циклом, в котором каждому предыдущему состоянию всех переменных $X_{k-1}$ находится последующее $X_k$ (окончание доказательства п.2.1). Поэтому, когда он закончит свою работу, целевое условие $G(X_k)$ станет истинным. Отсюда, нам необходимо взять выражение $\lnot G(X_k)$ перед началом каждого $k-го$ прохода:
Алгоритм 1:
$k \leftarrow 0 $ $X_0 = (x_0,y_0,...,z_0)$ $\mathbf{While} \lnot G(X_k)$ $\mathbf{do} $ $\mathbf{if}$ $I(X_k)$ $\mathbf{then}$ $X_k \leftarrow F(X_{k-1})$ $k \leftarrow k + 1$
2.4. По окончанию цикла соблюдается истинность инварианта и условия его окончания цикла
Обычно, при доказательстве инвариантности цикла используют более простой алгоритм:
Алгоритм 2:
$\\ k \leftarrow 0 $ $X_0 = (x_0,y_0,...,z_0)$ $\mathbf{While} \lnot Q(X_k) \land I(X_k)$ $\mathbf{do}$ $X_k \leftarrow F(X_{k-1})$ $k \leftarrow k + 1 $
Здесь вместо целевого условия $G(X_k)$ используется условие окончания цикла $Q(X_k)$, которое с одной стороны упрощает алгоритм цикла, но с другой – затрудняет доказательство его инвариантности.
Дело в том, что целевое условие цикла $G(X_k)$ и условие его окончания $Q(X_k)$ являются с точки зрения логики доказательства двумя разными событиями, хотя по смыслу являются одним и тем же. Поэтому при написании программного кода они реализуются через одно и то же условие, принимающее "ИСТИНУ" или "ЛОЖЬ".
Таким образом, несмотря на единство двуличия, можно преобразовать наш первый алгоритм, приведенный ранее в п.2.3.
Алгоритм 3:
$k \leftarrow 0$ $X_0 = (x_0,y_0,...,z_0)$ $\mathbf{While} \lnot G(X_k)$ $\mathbf{do}$ $X_k \leftarrow F(X_{k-1})$ $\mathbf{if} \ \lnot Q(X_k) \land I(X_k) $ $\mathbf{then}$ $ k \leftarrow k + 1 $ $\mathbf{ G(X_k) \Leftarrow Q(X_k) \land I(X_k)}$
В алгоритме 3 одновременная истинность инварианта $I(X_k)$ и условия окончания цикла $Q(X_k)$ влекут наступление целевого условия $G(X_k)$, истинность которого неизбежно приведет к его завершению и одновременно доказывая, что цикл завершится в том случае, если наступит условие его завершения $Q(X_k)$ при одновременной истинности инварианта $I(X_k)$, тем самым доказывается инвариантность цикла и верность выбранного алгоритма.
3. От теории к практике
На практике, производить все проверки не всегда оптимально, особенно на критических участках кода, где требуется высокая оптимизация. Поэтому преобразуем третий алгоритм следующим образом:
Алгоритм 4:
$\\ k \leftarrow 0$ $X_0 = (x_0,y_0,...,z_0)$ $\require{cancel}\bcancel{\mathbf{While} \lnot G(X_k)}$ $\mathbf{While} \lnot Q(X_k) \land I(X_k)$ $\mathbf{do}$ $X_k \leftarrow F(X_{k-1})$ $\require{cancel} \bcancel{\mathbf{If} \ I(X_k)}$ $\bcancel{\mathbf{then}}$ $ k \leftarrow k + 1 $ $\require{cancel} \bcancel{\mathbf{ G(X_k) \Leftarrow Q(X_k) \land I(X_k)}}$
Как видно из алгоритма 4 из него исключена оценка наступления целевого условия цикла $G(X_k)$, так как оно согласно п.2.4 тождественно условию окончанию цикла $Q(X_k)$ и проверки на истинность инварианта $I(X_k)$:
$G(X_k) \equiv Q(X_k) \land I(X_k) $
При этом было бы разумным оставить проверку истинности инварианта $I(X_k)$, при котором производится увеличение счетчика проходов цикла $k$, но алгоритм 2 её делает избыточной, так как в начале каждого прохода это делается неизбежно.
4. От практики к реализации
В языке программирования GNU C, для работы с рекуррентными циклами используются операторы while, do и for. При этом, цикл реализованный через операторы while и for подразумевают, что цикл инвариантен до первого прохода. Иначе, в соответсвие с описанием for и while, они завершаться ещё до первого прохода, в то время как do предлагает это делать в конце выполнения цикла вместе с проверкой на условие его завершения $Q(X_k)$.
4.1 Оператор for
Данный оператор предполагает в одной записи сразу несколько действий:
Действие 1 (initialize)
инициализирует общий набор переменных $X_0=(x_0,y_0,...,z_0)$, т.е. присваивает начальное состояния переменным до вхождения в цикл, когда $k \leftarrow 0$;
Действие 2 (test)
осуществляет проверку на условие завершения $Q(X_k)$ и (или) истинность инварианта $I(X_k)$ перед выполнением первого прохода, когда $k \leftarrow 0$, поэтому перед первым проходом и последующим будем проводить проверку на условие завершения цикла $Q(X_k)$ и истинности инварианта $I(X_k)$, что не противоречит ранее доказанным утверждениям инвариантности цикла в п.п 2.2 и 2.3;
Действие 3 (statement)
производит изменение состояние переменных $X_{k+1} \leftarrow F(X_k)$
Действие 4 (step)
изменяет значение счетчика проходов $k$ на один, т.е. $k \leftarrow k + 1$
Таким образом, основная форма записи может иметь следующий вид:
Форма записи 1:
$\mathbf{for} ( initialize; test; step )$ $statement$ Где $initialize:$ $X_0=(x_0,y_0,...,z_0)$, $ k \leftarrow 1$ $test:$ $\ \lnot Q(X_k) \land I(X_k)$ $statement:$ $X_k \leftarrow F(X_{k-1})$ $step:$ $k \leftarrow k + 1$
Учитывая, что проверка на истинность инварианта $I(X_k)$ может производится до присвоения состояний набору переменных $X_k$, поэтому в форму записи 1 можно привести к следующему:
Форма записи 1а:
$\mathbf{...}$ $test:$ $\ \lnot Q(X_k)$ $statement:$ $\mathbf{if}$ ( $I(X_k)$ ) { $X_k \leftarrow F(X_{k-1})$ }else $\mathbf{break};$ $\mathbf{...}$
Таким образом, форма записи 1a доказывает право на жизнь алгоритма 4 с одним отличаем, что цикл будет принудительно завершен из-за отсутствия истинности инварианта $I(X_k)$. Также в этом случае можно насильно присваивать false условию окончания цикла $Q(X_k)$, но быстрее будет воспользоваться оператором break, который немедленно завершит цикл.
Листинг 1:
#define CARRAY_LEN 11
char carray_buf[CARRAY_LEN] = { 0x30 }, /* массив символов содержит
следующие их коды символов:
'0','1'-'9' и ':' */
*go_p = (char *)carray_buf+1; /* смещение на незаписанный символ,
потому что начальное состояние X[k]
инвариантно */
int i;
/* проверка на условие окончание цикла осуществляется
в test */
for ( i=1 ; !ispunct(*go_p); i++, go_p++ ) {
*go_p = *(go_p-1) + 1;
if( isdigit(*go_p) ) { /* проверка на истинность инварианта */
fprintf(stdout,"Step %d: '%c'(%02X)\n", i, *go_p, *go_p );
}else
break;
}
fprintf(stdout,"Step %d: end of loop.\n", i );
Если же условия завершения $Q(X_k)$ и истинности инварианта $I(X_k)$ тождественны, то может иметь место следующая запись:
Форма записи 2:
$\mathbf{for} ( initialize;; step )$ $statement$ Где $initialize:$ $X_0=(x_0,y_0,...,z_0)$, $ k \leftarrow 1$ $statement:$ $\mathbf{if}$ ( $I(X_k)$ ) { $X_k \leftarrow F(X_{k-1})$ }else $\mathbf{break};$ $step:$ $k \leftarrow k + 1$
Здесь проверка на условие завершения $Q(X_k)$ опущена, так как проводится одновременно с проверкой на условие истинности инварианта $I(X_k)$.
Ниже, в листинге 2 приводится код реализации рекуррентного цикла для формы записи 2.
Листинг 2:
char carray_buf[CARRAY_LEN] = { 0x30 }, /* массив символов содержит
следующие их коды символов:
'0','1'-'9' и ':' */
*go_p = (char *)carray_buf+1; /* смещение на незаписанный символ,
потому что начальное состояние X[k]
инвариантно */
int i;
for ( i=1 ; ; i++, go_p++ ) {
*go_p = *(go_p-1) + 1;
if( isdigit(*go_p) ) { /* проверка на истинность инварианта */
fprintf(stdout,"Step %d: '%c'(%02X)\n", i, *go_p, *go_p );
continue;
}
if ( ispunct(*go_p) ) { /* Проверка на условие окончание цикла */
fprintf(stdout,"Step %d: end of loop.\n", i );
break;
}
}
Последовательность символов для их кодировок в ascii и её расширения utf-8 всегда будет следующей:
| Базовый код/ смещение | +00h | +01h | +02h | +03h | +04h | +05h | +06h | +07h | +08h | +09h | +0Ah |
| 0030h | '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' | ':' |