Главная Случайная страница Контакты | Мы поможем в написании вашей работы! | ||
|
Пусть имеется вызов предиката
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). □
Дата публикования: 2014-11-18; Прочитано: 204 | Нарушение авторского права страницы | Мы поможем в написании вашей работы!