Конструктор массива является базисным предикатом ConsArray(x, B: A), где x - возможно пустой набор переменных, B - имя предиката, отличное от ConsPred и ConsArray. Значением переменной A предикатного типа (4.7) является новый массив, создаваемый при исполнении вызова предиката ConsArray. Логическая семантика предиката ConsArray дается определением
LS(ConsArray(x, B: A)) @ "y"z. (LS(A(y: z)) º LS(B(x, y: z))) . (4.27)
Здесь x, y и z - произвольные непересекающиеся наборы переменных, причем набор x может быть пустым, а y и z не пусты. Значения y называются индексами, а z - элементами массива. Переменная A имеет предикатный тип PRED(Y: Z), где Y и Z - наборы типов, соответствующие наборам переменных y и z. Типы набора Y являются конечными. Произвольный массив j Î PRED(Y: Z) определен для любого набора индексов, т. е. истинно "y Î Y $z Î Z j(y: z).
Логическая семантика ConsArray (4.27) и ConsPred (4.23) идентична, однако отличается исполнение. Пусть вызов ConsArray(x, B: A) находится в правой части определения некоторого предиката, исполняемого в рамках секции s. Секция s включает набор x и переменную A, значением которой является массив A~, т. е. s[A] = A~. Массив A~ кодирует предикат A следующим образом:
A(y: z) º A~[y] = z . (4.28)
Исполнение вызова ConsArray(x, B: A) является частным случаем исполнения вызова
runCall(s, ConsPred(x, B: A)) (см. разд. 4.4) и реализуется следующими операторами:
s[A] = newArray(Y, Z); (4.29)
forAll yÎY do runCall(s, B(x, y: s[A][y])) end .
Первый оператор создает в памяти массив A~ как значение типа PRED(Y: Z). Массив становится значением переменной A в секции s. Оператор forAll реализует полный перебор наборов индексов, принадлежащих набору типов Y, и для каждого набора индексов y исполняет тело оператора forAll, причем исполнение тела для разных y может проводиться параллельно. Для каждого набора y значение результата вызова предиката B присваивается элементу A~[y]. Допустим, эффект оператора S(y: z) определяется формулой F(y). Тогда эффект оператора forAllyÎY do S(y: z) end есть
"yÎY. F(y) . (4.30)
Лемма 4.8. Cons(A). Доказательство непосредственно следует из соотношения (4.28). □
Лемма 4.9. Допустим, предикат B(x, y: z) определяет однозначную всюду определенную функцию по x и y, т. е. истинно условие
"x "y Î Y $!z B(x, y: z) . (4.31)
Тогда Cons(B) Þ Cons(ConsArray).
Доказательство. Пусть истинно Cons(B). Зафиксируем x. В соответствии с (4.30) после исполнения оператора forAll из (4.29) будет истинной формула: "yÎY. B(x, y: A~[y]). Пусть z - тот единственный набор, для которого истинно B(x, y: z) в соотношении (4.31). Тогда A~[y] = z. Из (4.28) следует истинность A(y: z). В итоге, после исполнения тела forAll будет истинно "yÎY. B(x, y: z) & A(y: z). Поскольку z единственно для B(x, y: z) и A(y: z), то будет истинным "yÎY. B(x, y: z) º A(y: z). Дальнейшее доказательство очевидно. □
Допустим, в секции s исполняется вызов предиката A(u: v), где A является переменной предикатного типа, а значением A является массив. Секция s содержит переменную A и наборы u и v. Исполнение вызова A(u: v) реализуется следующим оператором:
s[v] := s[A] [u] .
Для исполнения вызова A(u: v) в разд. 4.4 принято обозначение runCall(s, A(u: v)).