Условный оператор. Условный оператор является правой частью следующего определения предиката:

Условный оператор является правой частью следующего определения предиката:

A(b, x: y) º if ( b) B(x: y) else C(x: y). (4.20)

Здесь x и y - произвольные непересекающиеся наборы переменных, причем набор x может быть пустым, b - переменная логического типа, не встречающаяся в наборах x и y. Если B или C есть имя переменной предикатного типа, то оно входит в набор x. Логическая семантика условного оператора представлена следующим образом:

LS(if ( b) B(x: y) else C(x: y)) @ (b Þ B(x, y)) & (Øb Þ C(x, y)). (4.21)

Допустим, определение предиката A исполняется в рамках секции s. Секция s включает переменную b и переменные наборов x и y. Исполнение правой части определения (4.20) соответствует оператору runStat(s, K(x: y)) в (4.14) и определяется следующим образом:

if (s[b]) runCall(s, B(x: y)) else runCall(s, C(x: y)). (4.22)

Таким образом, алгоритм исполнения условного оператора зависит от значения переменной b. Если значение b истинно, исполняется вызов предиката B. В противном случае исполняется вызов предиката C.

Лемма 4.5. Cons(B) & Cons(C) Þ Cons(H), где H(b, x: y)

обозначает if ( b) B(x: y) else C(x: y).

Доказательство. Пусть истинно Cons(B) и Cons(C). Докажем истинность Cons(H). Зафиксируем значения b, x и y. Пусть истинна H(b, x: y). Тогда в соответствии с (4.21) истинны формулы b Þ B(x: y) и Øb Þ C(x: y). Рассмотрим случай, когда значение b истинно. Тогда истинна формула B(x: y). Из Cons(B) следует, что исполнение вызова B(x: y) завершается получением набора y. Поэтому исполнение оператора (4.22), а значит и H(b, x: y), завершается вычислением y. Это доказывает первую часть свойства Cons(H) для истинного значения b. Доказательство в случае ложного значения b проводится аналогично.

Допустим, исполнение H(b, x: y) завершается вычислением y, т. е. исполнение оператора (4.22) завершается вычислением y. Докажем истинность H(b, x: y). Пусть b истинно. Тогда исполнение вызова B(x: y) завершается получением набора y. Из Cons(B) следует истинность B(x: y). Тогда истинны формулы b Þ B(x: y) и Øb Þ C(x: y), поскольку b истинно. Следовательно, истинна правая часть (4.21) и H(b, x: y). Доказательство истинности H(b, x: y) в случае ложного значения b проводится аналогично. □