Пусть имеется вызов предиката
A(z:u) . (4.12)
Здесь A есть имя предиката или имя переменной предикатного типа; z - возможно пустой набор имен переменных; u - непустой набор имен переменных. Для случая, когда A - имя предиката, рассмотрим соответствующее определение предиката A:
A(x:y) º K(x:y) , (4.13)
где x и y - наборы переменных, причем все переменные различны; K(x:y) - оператор. Пусть вызов (4.12) находится в правой части определения предиката B. Допустим, что определение предиката B исполняется в секции q. Тогда переменные наборов z и u принадлежат секции q. Исполнение вызова A(z:u) будем записывать на метаязыке в виде вызова процедуры runCall(q, A(z:u)), тело которой представлено ниже:
s = newSect(A); (4.14)
s[x] := q[z];
runStat(s, K(x:y));
q[u] := s[y] .
В теле runCall сначала создается секция s для переменных определения A. Значения аргументов z вызова A(z:u) копируются в аргументы x определения A. В рамках секции s исполняется оператор K(x:y), что на метаязыке представлено вызовом runStat(s, K(x:y)). Наконец, результаты y копируются в результаты вызова u. Если в вызове (4.12) A есть имя переменной предикатного типа, то в теле (4.14) вместо первого оператора исполняется s = newSect(q[A]).
Поскольку секции s и q различны, а исполнение runStat(s, K(x:y)) не меняет содержимое секции q, при завершении исполнения тела (4.14) будет истинным соотношение
x = z& u =y . , (4.15)
Если предикат A является базисным, то вызов A(z:u) считается элементарным оператором абстрактного процессора, и для его исполнения не требуется исполнять тело (4.14). Тем не менее, и в этом случае исполнение вызова A(z:u) будем обозначать через
runCall(q, A(z:u)). Исполнение вызова A(z:u) для случая, когда A является переменной предикатного типа, а значением A - массив, определено в разд. 4.9.
Лемма 4.2. Пусть имеется определение (4.13) для предиката A. Тогда Cons(K) Þ Cons(A). Отметим, что здесь Cons(A) относится к произвольному вызову A(z:u) для некоторых наборов z и u.
Доказательство. Пусть истинно Cons(K). Докажем истинность Cons(A). Зафиксируем значения наборов z и u. Пусть истинно A(z:u). Тогда в соответствии с определением (4.13) истинна формула K(z:u). Из этого следует, что существует исполнение K(z:u) для набора z, которое завершается получением набора u. При завершении исполнения тела (4.14) в соответствии с (4.15) справедливы равенства x = z и u = y. Поэтому существует исполнение K(x:y), завершающееся получением y. Тогда исполнение последовательности (4.14), а значит и исполнение A(z:u), завершается получением значений набора u, что доказывает первую часть свойства Cons(A).
Пусть исполнение A(z:u) для набора z завершается получением набора u. Тогда завершается исполнение тела (4.14), в частности исполнение K(x:y) завершается получением y. Поскольку в соответствии с (4.15) реализуются равенства x = z и u = y, то исполнение K(z:u) завершается вычислением набора u. Из Cons(K) следует, что K(z:u) истинно. Тогда из определения (4.13) следует истинность A(z:u), что доказывает вторую часть свойства Cons(A). □