Однозначность предикатов

Применимость правил серии L доказательства корректности программы в соответствующих леммах базируется на однозначности операторов, используемых в определениях предикатов. Покажем, что однозначность операторов гарантируется в случае однозначности базисных предикатов, используемых в определениях программы.

Лемма 4.17. Оператор суперпозиции (4.16), параллельный оператор (4.19) или условный оператор (4.20) является однозначным, если вызываемые в операторе предикаты B и C являются однозначными.

Лемма 4.18. Пусть имеется рекурсивное кольцо предикатов (4.36). Кроме рекурсивных предикатов A₁, A₂,…,A_n, в правых частях определений кольца предикатов используются предикаты E₁, E₂,…, E_s. Предположим, что предикаты E₁, E₂,…, E_s являются однозначными. Если аргумент определения кольца имеет предикатный тип, то предикат, являющийся значением аргумента, считается однозначным. Тогда рекурсивные предикаты A₁, A₂,…,A_n кольца (4.36) являются однозначными.

Доказательство. Из-за ограничений на сложные формы рекурсии предикат, являющийся значением аргумента, не может входить в кольцо предикатов. Поэтому можно считать, что такой предикат находится среди E₁, E₂,…, E_s.

Пусть D(u: v) - рекурсивный предикат кольца, т. е. D = A_j для некоторого j. Допустим, истинны D(u: v1) и D(u: v2). Необходимо доказать, что v1 = v2. В соответствии с леммой 4.13 существует m, при котором D^m(u: v1) и D^m(u: v2) истинны. Поэтому достаточно доказать, что каждый элемент A^m цепи {A^m}_m³0, определенной в (4.41), является вектором однозначных предикатов. Доказательство проводится индукцией по m.

Элемент A⁰ является вектором однозначных предикатов, поскольку тотально ложный предикат F является однозначным. Допустим, по индуктивному предположению, A^m-1 является вектором однозначных предикатов. Докажем это свойство для A^m. В правой части каждого определения из A^m используется оператор суперпозиции (4.16), параллельный оператор (4.19) или условный оператор (4.20). Вызываемые предикаты в правой части:
A^m-1₁, A^m-1₂,…,A^m-1_n и E₁, E₂,…, E_s - однозначны. Однозначность компонент A^m следует из леммы 4.17. □

Базисные предикаты ConsPred и ConsArray не являются однозначными. В двух разных исполнениях вызова ConsPred(x, B: A) (при совпадающих x и B) в качестве значения переменной A будут получены разные имена. Однако при этом предикаты, обозначаемые разными именами, будут тождественны. Это обеспечивает однозначность вызовов предиката A при условии, что предикат B является однозначным. Аналогично будет однозначным предикат, порождаемый вызовом предиката ConsArray.

Лемма 4.19. В соответствии с правилами S1-S4 построения заместителей любой вызов C(…) в программе, где C - переменная предикатного типа, является однозначным, если для каждого вызова конструктора ConsPred(x, B: A) или ConsArray(x, B: A) предикат B является однозначным.

Теорема 4.2. Допустим, всякий базисный предикат языка CCP, кроме ConsPred и ConsArray, является однозначным на всем множестве значений аргументов. Пусть имеется программа на языке CCP, и ее исполнение реализуется вызовом предиката D(u: v), причем в наборе v нет переменных предикатного типа. Тогда предикат D является однозначным.

Доказательство. Сначала доказательство проводится для программы, в которой нет переменных предикатного типа.

Рассмотрим случай, когда программа не содержит рекурсивно определяемых предикатов. Если предикат D - базисный, то его однозначность гарантируется условием теоремы. Пусть предикат D имеет определение в виде оператора суперпозиции (4.16), параллельного оператора (4.19) или условного оператора (4.20). В соответствии с леммой 4.17 достаточно установить однозначность предикатов B и C, вызываемых в правой части определения. Если эти предикаты базисные, то их однозначность является условием теоремы. Если один из них - определяемый, то его полное замкнутое определение представляется частью программы меньшего размера, что позволяет применить доказательство по индукции.

Допустим, в программе имеются рекурсивно определяемые предикаты. В соответствии с анализом, проведенным при доказательстве теоремы 4.1, совокупность рекурсивно определяемых предикатов образует дерево колец. Для колец, являющихся листьями дерева, однозначность следует из леммы 4.18. Доказательство однозначности предикатов остальных колец проводится индукцией по длине пути в дереве колец. Отметим, что доказательство легко обобщается для случая, когда в программе имеются переменные предикатного типа, значениями которых являются однозначные предикаты.

Допустим, в программе П имеются переменные предикатного типа. Обозначим через SUBS(П) набор предикатов, являющийся объединением множеств заместителей для всех переменных предикатного типа в программе П. Для набора предикатов M из П обозначим через П[M] минимальную программу, являющуюся частью П и содержащую определения предикатов набора M. Пусть П₀ = П, П_j+1 = П_j[SUBS(П_j)], j = 0, 1, 2, …. В теореме 4.1 доказано, что для некоторого k программа П_k ¹ Æ, а П_k+1 = Æ. Программа П_k не содержит переменных предикатного типа. Однозначность предикатов программы П_k доказана выше. Тогда предикаты B₁, B₂,…, B_n, входящие в SUBS(П_k-1), являются однозначными. В соответствии с леммой 4.19 любой вызов вида C(…) в программе П_k-1, где C - переменная предикатного типа, является однозначным. Доказательство теоремы, представленное выше, обобщается для программы П_k-1, поскольку согласно принятым ограничениям вызов вида C(…) не может участвовать в рекурсии. Доказательство теоремы для произвольной программы
П_i, i = k - 1, …, 0, проводится по индукции. □

Список литературы

1. Backus J. Can programming be liberated from the von Neumann style? A. Functional Style and Its Algebra of Programs // Communications of the ACM. 1978. Vol. 21 (8). P. 613–641.

2. Hoare C. A. R. О структурной организации данных // Структурное программирование. М.: Мир, 1975. С. 98-197.

3. Tennent R. D. Semantics of Programming Languages. Pentice Hall, 1991. 236 p.

4. Крицкий С. П. Трансляция языков программирования: синтаксис, семантика, перевод: Учеб. пособие. Р.-на-Дон.: РГУ, 2005.

URL: http://public.uic.rsu.ru/~skritski/scourses/Transl/Langs1.htm.

5. Гретцер Г. Общая теория решеток: Пер. с англ. 1982. 456 с.

7. Лавров С. С. Программирование. Математические основы, средства, теория. СПб.: БХВ-Петербург, 2001. 320 с.

8. Milner R. A Calculus of Communicating Systems // Lecture Notes in Computer Science. 1980.Vol. 92.

9. Hoare C. A. R.. Communicating Sequential Processes. Prentice-Hall. 1985.

5. Семантика языка предикатного программирования.
Методы доказательства корректности предикатных программ

Язык CCP (язык исчисления вычислимых предикатов; см. разд. 4) определяет минимальное полное ядро для построения произвольного (чистого) языка функционального программирования в виде иерархической системы обозначений на базе конструкций ядра. Язык предикатного программирования P (Predicate programming language) конструируется как результат последовательного расширения цепочки языков (слоев):

CCP = P0 Ì P1 Ì P2 Ì P3Ì... Ì P.

Каждый очередной слой языка определяется в виде набора производных конструкций от предыдущего слоя.

Каждая новая конструкция C очередного слоя вводится как обозначение некоторой языковой композиции K предыдущего слоя. Логическая семантика LS(C) новой конструкции получается тождественным логическим преобразованием формулы LS(K), а операционная семантика - эквивалентным преобразованием метапрограммы для композиции K. Такой механизм построения логической и операционной семантики конструкции C гарантирует их согласованность в соответствии с определением (4.11). В большинстве случаев правила доказательства корректности конструкции C удается построить преобразованием соответствующих правил для композиции K. Предлагается две серии правил: R и L. Серия R определяет правила доказательства истинности постусловия из программы по формуле (2.10). Серия L определяет правила вывода программы из спецификации по теореме 2.1 тождества спецификации и программы; в этой теореме требуется однозначность программы и спецификации. Однозначность операторов программы гарантируется в случае однозначности базисных предикатов в соответствии с теоремой 4.2.

5.1. Язык P1: подстановка определения предиката на место вызова

Определим подстановку определения предиката A(x: y) º K(x: y) (см. (4.2)) на место вызова A(t: z), где x, y, t и z - наборы переменных. Результатом подстановки является конструкция { K(t: z) }, называемая блоком, которая вставляется в программу на место вызова A(t: z). Конструкция K(t: z) получается из K(x: y) заменой всех вхождений переменных наборов x и y на соответствующие переменные наборов t и z. Здесь и далее мы полагаем, что для любого определения предиката параметры и локальные переменные имеют уникальные имена, не встречающиеся в других определениях программы. Кроме того, если K(x: y) - оператор суперпозиции, то при построении блока { K(t: z) } дополнительно проводится переименование локальных переменных, обеспечивающее их уникальность. С учетом данных соглашений замена x и y на t и z в конструкции K(x: y) не приведет к коллизиям. Определим

LS({ K(t: z) }) @ LS(K(t: z)). (5.1)

Поскольку A(t: z) º K(t: z), то LS({ K(t: z) }) º LS(A(t: z)).

Исполнение блока { K(t: z) } в секции s определяется на метаязыке вызовом
runBlock(s, { K(t: z) }). Тело процедуры runBlock представлено оператором

runStat(s, K(t: z)). (5.2)

Исходя из операционной семантики вызова предиката (4.14) нетрудно показать, что исполнение вызова A(t: z) эквивалентно исполнению блока { K(t: z) }. Таким образом, программа П’, получаемая из программы П подстановкой определения предиката на место вызова, эквивалентна программе П: исполнение любого предиката программы П’ на фиксированном наборе аргументов дает тот же результат, что и в программе П.

Язык программы, получающийся многократным произвольным применением подстановок определений предикатов на место вызовов, обозначим через P1. Язык P1 является расширением языка CCP. В языке P1 правой частью определения предиката является оператор суперпозиции (4.16), параллельный оператор (4.19) или условный оператор (4.20), причем в данных операторах на месте вызовов предикатов B и C может также находиться конструкция «блок». Блок может содержать блоки внутри себя. По построению конструкции языка P1 (операторы и блоки), полученные подстановками определений предикатов на место вызовов, обладают свойством согласованности.

5.2. Язык P2: оператор суперпозиции и параллельный оператор общего вида

Операторы { A(…); B(…) }; C(…) и A(…); { B(…); C(…) } являются эквивалентными, т. е. суперпозиция обладает свойством ассоциативности. Это доказывается на основе операционной семантики оператора суперпозиции (4.18). Аналогичным образом устанавливается ассоциативность параллельной композиции, т. е. эквивалентность { A(…) ½½ B(…) } ½½ C(…) и A(…) ½½ { B(…) ½½ C(…) }. Свойство ассоциативности позволяет опускать внутренние фигурные скобки. Введем в языке P2 оператор суперпозиции и параллельный оператор общего вида: A₁(…); A₂(…); …; A_n(…) и A₁(…) ½½ A₂(…) ½½ … ½½ A_n(…) для n > 1.

Рассмотрим оператор суперпозиции общего вида со спецификацией в виде предусловия P(x) и постусловия Q(x, y):

P(x) {B1(x: z₁); B2(z₁: z₂);...; Bj(z_j-1: z_j);...; Bn(z_n-1: y)} Q(x, y) [18]. (5.3)

Здесь x, z₁, z₂, …, z_n-1, y - различные непересекающиеся наборы переменных; B1, B2, …, Bn обозначают вызовы предикатов или блоки языка P1 со спецификациями (предусловиями и постусловиями) P_B1(x), Q_B1(x, z₁), P_B2(z₁), Q_B2(z₁, z₂), …, P_Bn(z_n-1), Q_Bn(z_n-1, y). Логическая семантика оператора суперпозиции общего вида определяется на основе логической семантики суперпозиции двух операторов (4.17):

LS(B1(x: z₁); B2(z₁: z₂);...; Bj(z_j-1: z_j);...; Bn(z_n-1: y)) º

$z₁,z₂,...,z_n-1. LS(B1(x: z₁)) & LS(B2(z₁: z₂)) &...& LS(Bj(z_j-1: z_j)) &...& LS(Bn(z_n-1: y)). (5.4)

Допустим, определение предиката A исполняется в рамках секции s. Секция s состоит из переменных наборов x, y и z₁, z₂,..., z_n-1. Исполнение оператора (5.3) реализуется на метаязыке оператором runStat(s, B1(x: z₁); …; Bn(z_n-1: y)) в (4.14) и определяется следующим образом:

runCallBlock(s, B1(x: z₁)); (5.5)

runCallBlock(s, B2(z₁: z₂));.....;

runCallBlock(s, Bj(z_j-1: z_j));.....;

runCallBlock(s, Bn(z_n-1: y)).

Здесь runCallBlock обозначает runCall, если вторым параметром является вызов предиката, или runBlock в случае блока.

Определим правила серии L, гарантирующие корректность оператора суперпозиции общего вида (5.3).

Правило LS3. P(x) ├ P_B1(x).

Правило LS4. P(x) & Q(x, y) & Q_B1(x, z₁) ├

$!z₂,z₃,...,z_n-1. P_B2(z₁) & Q_B2(z₁, z₂) &...& P_Bj(z_j-1) & Q_Bj(z_j-1, z_j) &...& P_Bn(z_n-1) & Q_Bn(z_n-1, y).

Лемма 5.1. Допустим, спецификация P(x) и Q(x, y) оператора суперпозиции общего вида реализуема, операторы B1, …, Bn однозначны в области предусловий и корректны, а их спецификации однозначны. Если правила LS3 и LS4 истинны, то оператор суперпозиции (5.3) является корректным.

Доказательство. Поскольку операторы B₁, …, B_n однозначны, то и оператор суперпозиции (5.3) является однозначным. В соответствии с (5.4) и теоремой 2.1 для доказательства леммы достаточно доказать истинность формулы

P(x) & Q(x, y) Þ

$z₁,z₂,...,z_n-1. LS(B1(x: z₁)) & LS(B2(z₁: z₂)) &...& LS(Bj(z_j-1: z_j)) &...& LS(Bn(z_n-1: y)). (5.6)

Пусть истинны P(x) и Q(x, y). Докажем истинность правой части (5.6). Из истинности предусловия P(x) по правилу LS3 следует истинность P_B1(x). Из корректности оператора B1 по правилу E2 следует истинность формулы $z₁. LS(B1(x: z₁)). Допустим, для некоторого z’₁ истинно LS(B1(x: z’₁)). Для оператора B1 истинны условия леммы 2.8. Поэтому истинно Q_B1(x, z’₁). В соответствии с правилом LS4 истинна правая часть LS4 для z₁ = z’₁. Тогда из истинности P_Bj(z_j-1) & Q_Bj(z_j-1, z_j) для j = 3,…, n (z_n = y) по лемме 2.9 следует истинность LS(Bj(z_j-1: z_j)). Это доказывает истинность формулы (5.6). □

Определим правила серии R, гарантирующие корректность оператора суперпозиции общего вида (5.3).

Правило RS3. P(x) ├ P_B1(x) & "z₁,z₂,..., z_n-1.

(Q_B1(x, z₁) Þ P_B2(z₁)) & (Q_B2(z₁, z₂) Þ P_B3(z₂)) &... & (Q_Bn-1(z_n-2, z_n-1) Þ P_Bn(z_n-1)).

Правило RS4. P(x) & $z₁,z₂,...,z_n-1 (Q_B1(x, z₁) & Q_B2(z₁, z₂) &... & Q_Bn(z_n-1, y)) ├

Q(x, y).

Лемма 5.2. Пусть предусловие P(x) истинно. Допустим, операторы B1, …, Bn корректны. Если правила RS3 и RS4 истинны, то оператор суперпозиции (5.3) является корректным.

Доказательство. В соответствии с формулой (2.10) достаточно доказать реализуемость LS(B1; B2; …, Bn)(x, y) и выводимость постусловия Q(x, y) из LS(B1; B2; …, Bn)(x, y). Вместо LS(B1; B2; …, Bn)(x, y) рассматривается правая часть (5.4).

Из истинности предусловия P(x) по правилу RS3 следует истинность правой части правила, в том числе формулы P_B1(x). Из истинности P_B1(x) и правила E2 следует истинность формулы $z. LS(B1(x: z)). Допустим, для некоторого z’₁ формула LS(B1(x: z’₁)) истинна. Из истинности P_B1(x) и правила E3 следует истинность LS(B1(x: z’₁)) Þ Q_B1(x, z’₁). Как следствие, истинно Q_B1(x, z’₁). Из истинности правой части RS3 следует истинность формулы "z₁ (Q_B1(x, z₁) Þ P_B2(z₁)). Как следствие, истинно P_B2(z’₁). По правилу E2 истинна формула $z₂ LS(B2)(z’₁, z₂). Пусть формула истинна для z’₂. Из истинности Q_B2(z₁, z₂) Þ P_B3(z₂) следует истинность P_B3(z’₂). Аналогичным образом, по индукции доказывается истинность LS(Bj(z_j-1: z_j)) для j = 1,…, n - 1. Это доказывает реализуемость LS(B1; B2; …, Bn)(x, y).

Допустим, истинна правая часть (5.4). Докажем истинность постусловия Q(x, y). Пусть правая часть (5.4) истинна для z’₁, z’₂,..., z’_n-1. По правилу E3 истинна формула LS(B1(x: z’₁)) Þ Q_B1(x, z’₁) и далее – Q_B1(x, z’₁). Истинность Q_B1(x, z’₁) и "z (Q_B1(x, z) Þ P_B2(z)) влечет истинность P_B2(z’₁). По правилу E3 истинно LS(B2(z’₁: z’₂)) Þ Q_B2(z’₁, z’₂). Поскольку LS(B2(z’₁: z’₂)) истинно, то истинно Q_B2(z’₁, z’₂). Аналогичным образом по индукции доказывается истинность Q_Bj(z’_j-1, z’_j) для j = 2, …, n - 1. Таким образом, истинна правая часть правила RS4, а значит, и левая, т. е. истинно постусловие Q(x, y). □

Рассмотрим параллельный оператор общего вида со спецификацией в виде предусловия P(x) и постусловия Q(x, y):

P(x) {B1(x: y₁) || B2(x: y₂) ||...|| Bj(x: y_j) ||...|| Bn(x: y_n)} Q(x, y). (5.7)

Здесь x, y₁, y₂, …, y_n - различные непересекающиеся наборы переменных; набор y объединяет в себе наборы y₁, y₂, …, y_n; B1, B2, …, Bn обозначают предикаты и блоки языка P1 со спецификациями (предусловиями и постусловиями) P_B1(x), Q_B1(x, y₁), P_B2(x), Q_B2(x, y₂), …, P_Bn(x), Q_Bn(x, y_n). Логическая семантика параллельного оператора общего вида определяется на основе логической семантики для двух операторов (см. разд. 4.6):

LS(B1(x: y₁) || B2(x: y₂) ||...|| Bj(x: y_j) ||...|| Bn(x: y_n)) º

LS(B1(x: y₁)) & LS(B2(x: y₂)) &... & LS(Bj(x: y_j)) &... & LS(Bn(x: y_n)). (5.8)

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

runCallBlock(s, B1(x: y₁)) || (5.9)

runCallBlock(s, B2(x: y₂)) ||... ||

runCallBlock(s, Bj(x: y_j)) ||... ||

runCallBlock(s, Bn(x: y_n)).

Определим правила серии L, гарантирующие корректность параллельного оператора общего вида (5.7).

Правило LP4. P(x) ├ P_B1(x) & P_B2(x) &... & P_Bn(x).

Правило LP5. P(x) & Q(x, y) ├ Q_B1(x, y₁) & Q_B2(x, y₂) &... & Q_Bn(x, y_n).

Лемма 5.3. Допустим, спецификация P(x) и Q(x, y) параллельного оператора общего вида реализуема, операторы B1, …, Bn однозначны в области предусловий и корректны, а их спецификации однозначны. Если правила LP4 и LP5 истинны, то параллельный оператор (5.7) является корректным.

Определим правила серии R, гарантирующие корректность параллельного оператора общего вида (5.7).

Правило RP3. P(x) ├ P_B1(x) & P_B2(x) &... & P_Bn(x).

Правило RP4. Q_B1(x, y₁) & Q_B2(x, y₂) &... & Q_Bn(x, y_n) ├ Q(x, y).

Лемма 5.4. Пусть предусловие P(x) истинно. Допустим, операторы B1, …, Bn корректны. Если правила RP3 и RP4 истинны, то параллельный оператор (5.7) является корректным.

Условимся, что суперпозиция «связывает» сильнее, чем параллельная композиция; т. е. вместо {A(…); B(…)} ½½ C(…) в языке P2 будем писать A(…); B(…) ½½ C(…). Если в операторе A(x: y); {B(z: t) ½½ C(u: v)} набор y пересекается с набором z и не пересекается с набором u, то оператор эквивалентен {A(x: y); B(z: t)} ½½ C(u: v) или, с учетом соглашения о приоритетах, оператору A(x: y); B(z: t) ½½ C(u: v). Аналогичным образом оператор {A(x: y)½½B(z: t)};C(u: v) эквивалентен A(x: y) ½½ B(z: t); C(u: v), если наборы y и u не пересекаются.

5.3. Язык P2: другое обобщение оператора суперпозиции

Оператор B(x: z); C(z: y) определен как наиболее простая форма оператора суперпозиции; см. (4.16). Оператор B(x: z); C(x, z: y) является обобщением оператора суперпозиции. Применяя данное обобщение к оператору суперпозиции общего вида (5.3), получим оператор

P(x) {B1(x: z₁); B2(x, z₁: z₂);...; Bj(x, z_j-1: z_j);...; Bn(x, z_n-1: y)} Q(x, y). (5.10)

Логическая и операционная семантика, правила RS3, RS4, LS3, LS4 обобщаются, а леммы 5.1 и 5.2 аналогичным образом доказываются для оператора (5.10). Отметим, что оператор вида B(x: z); C(u, z: y), где набор u содержит часть переменных набора x, можно рассматривать как частный случай оператора B(x: z); C(x, z: y).

Наиболее общей формой суперпозиции двух операторов является оператор

A(x: t, y) º P(x) {B(x: z, t); C(x, z: y)} Q(x,t, y). (5.11)

Здесь x, y, z, t - различные непересекающиеся наборы переменных, причем наборы x и t могут быть пустыми; B и C обозначают предикаты или блоки языка P1 со спецификациями (предусловиями и постусловиями) P_B(x), Q_B(x, z, t), P_C(x, z), Q_C(x, z, y).

Оператор суперпозиции (5.11) можно определить через оператор суперпозиции (4.16) и параллельный оператор (4.19) языка CCP следующим образом. Введем определения предикатов B1 и C1:

B1(x: x1, z, t1) º P_B(x) {B(x: z, t1) || x1 = x} Q_B(x, z, t1) & x1 = x;

C1(x1, z, t1: y, t) º P_C(x1, z) {C(x1, z: y) || t = t1} Q_C(x1, z, y) & t = t1.

Поскольку B1(x: x1, z, t1); C1(x1, z, t1: t, y) º B(x: z, t); C(x, z: y), то справедливо другое определение предиката A:

A(x: t, y) º P(x) {B1(x: x1, z, t1); C1(x1, z, t1: t, y)} Q(x,t, y). (5.12)

Определение (5.12) по форме соответствует простейшему оператору суперпозиции (4.16). Подставим правую часть (5.12) в определение логической и операционной семантики (4.17, 4.18) и проведем эквивалентные преобразования. Получим логическую и операционную семантику оператора (5.11):

LS(B(x: z, t); C(x, z: y)) º $z. (LS(B(x: z, t)) & LS(C(x, z, y))). (5.13)

runCallBlock(s, B(x: z, t)); (5.14)

runCallBlock (s, C(x, z: y)).

Для определения (5.12) применимы леммы 2.5 и 2.11. Применим правила RS1 и RS2 для оператора в правой части (5.12). Получим следующие правила.

Правило RS1’. P(x) ├ P_B(x) & "x1, z, t1 ((Q_B(x, z, t1) & x1 = x) Þ P_C(x1, z)).

Правило RS2’. P(x) & $x1,z,t1 (Q_B(x1, z, t1) & x1 = x & Q_C(x1, z, y) & t = t1) ├

Q(x,t, y).

Эквивалентные преобразования RS1’ и RS2’ дают правила RS5 и RS6, по форме подобные правилам RS1 и RS2 для простейшего оператора суперпозиции (4.16).

Правило RS5. P(x) ├ P_B(x) & "z, t (Q_B(x, z, t) Þ P_C(x, z)).

Правило RS6. P(x) & $z (Q_B(x, z, t) & (Q_C(x, z, y)) ├ Q(x,t, y).

Как следствие, справедлива следующая лемма.

Лемма 5.5. Пусть предусловие P(x) истинно. Допустим, операторы B и C корректны. Если правила RS5 и RS6 истинны, то оператор суперпозиции (5.11) является корректным.

Оператор суперпозиции вида (5.11) можно обобщить для произвольного числа композируемых операторов. Обобщается логическая и операционная семантика, а также лемма 5.5.

Применим правила LS1 и LS2 для оператора в правой части (5.12). Получим следующие правила.

Правило LS1’. P(x) ├ P_B(x).

Правило LS2’. P(x) & Q(x, t, y) & Q_B(x, z, t1) & x1 = x ├

P_C(x1, z) & Q_C(x1, z, y) & t = t1.

Эквивалентные преобразования LS1’ и LS2’ дают правила LS6 и LS7.

Правило LS6. P(x) ├ P_B(x).

Правило LS7. P(x) & Q(x, t, y) & Q_B(x, z, t1) ├ P_C(x, z) & Q_C(x, z, y) & t = t1.

Как следствие, справедлива следующая лемма.

Лемма 5.6. Допустим, спецификация оператора суперпозиции (5.11) реализуема, операторы B и C однозначны в области предусловий и корректны, а их спецификации однозначны. Если правила LS6 и LS7 истинны, то оператор суперпозиции (5.11) является корректным.

5.4. Язык P3: выражения

Наряду с предикатной (или операторной) формой представления конструкций будем использовать функциональную форму. Пусть имеется вызов предиката A(t: z), где t и z - наборы переменных. Как эквивалентную для вызова A(t: z) будем использовать запись в функциональном стиле: z = A(t). Конструкцию A(t) назовем вызовом функции. В случае, когда z - набор более чем из одной переменной, будем также использовать форму записи |z| = A(t).

Для базисных предикатов языка CCP, соответствующих стандартных арифметических операциям, вместо функциональной формы z = A(t) будем использовать традиционную инфиксную и постфиксную нотацию. Например, базисные предикаты: +(x, y: z), -(x, y: z),
-(x: y), <(x, y: b) - записываются в языке P3 привычным образом: z = x + y, z = x - y, y = -x, b = x < y.

В языке P3 вводятся изображения констант. Так, вместо базисных предикатов ConsIntZero(: x) и ConsIntOne(: x) используется запись вида x = 0 и x = 1. Значение x константы целого типа по ее изображению s определяется предикатом valInt(s: x). Например, x = 2089 интерпретируется как вызов valInt(“2089”: x). Аналогичным образом определяются изображения констант для других примитивных типов.

Применение функционального стиля позволяет преобразовать оператор суперпозиции следующим образом:

B(x: z); C(x, z: y) º z =B(x); C(x, z: y) º C(x, B(x): y).

В языке P3 аргументом вызова является либо переменная, либо вызов функции. При этом вызов функции в качестве аргумента определяется указанным тождеством. Семантика вызова, имеющего вызовы в двух и более аргументах, определяется следующим тождеством:

{ A(x: y) || B(z: t) }; C(y, t: u) º { y = A(x) || t = B(z) }; C(y, t: u) º C(A(x), B(z): u).

Таким образом, вычисление аргументов вызовов реализуется параллельно.

Определим правила доказательства корректности для вызова предиката, содержащего вызовы среди аргументов. Рассмотрим определение предиката

D(x, z: u) º P(x, z) {C(A(x), B(z): u)} Q(x, z, u). (5.15)

Пусть предикат A имеет спецификацию P_A(x) и Q_A(x, y), а предикат B - P_B(z) и Q_B(z, t). Если предикаты A и B являются корректными, то корректно следующее определение:

E(x, z: y, t) º P_A(x) & P_B(z) {A(x: y) || B(z: t)} Q_A(x, y) & Q_B(z, t).

Предикат D можно представить определением

D(x, z: u) º P(x, z) { E(x, z: y, t); C(y, t: u)} Q(x, z, u). (5.16)

Пусть предикат C со спецификацией P_С(y, t) и Q_С(y, t, u) является корректным. Применим правила RS1 и RS2 для оператора в правой части (5.16). Получим следующие правила.

Правило RS1’. P(x, z) ├ P_A(x) & P_B(z) & "y,t (Q_A(x, y) & Q_B(z, t) Þ P_C(y, t)).

Правило RS2’. P(x, z) & $y,t (Q_A(x, y) & Q_B(z, t) & Q_C(y, t, u)) ├ Q(x, z, u).

Допустим, операторы A и B являются однозначными; их спецификации P_A(x), Q_A(x, y), P_B(z), Q_B(z, t) также однозначны. Эквивалентные преобразования RS1’ и RS2’ с учетом однозначности предикатов и спецификаций позволяют устранить переменные y и t, что дает правила RS7 и RS8.

Правило RS7. P(x, z) ├ P_A(x) & P_B(z) & P_C(A(x), B(z)).

Правило RS8. P(x, z) & Q_C(A(x), B(z), u) ├ Q(x, z, u).

В итоге, справедлива следующая лемма.

Лемма 5.7. Пусть предусловие P(x, z) истинно. Допустим, операторы A, B и C корректны, операторы A и B, а также их спецификации P_A(x), Q_A(x, y), P_B(z), Q_B(z, t) однозначны. Если правила RS7 и RS8 истинны, то оператор (5.15) со спецификацией P(x, z) и Q(x, z, u) является корректным.

Для получения правил серии L применим правила LS1 и LS2 для оператора в правой части (5.16). Получим следующие правила.

Правило LS1’. P(x, z) ├ P_A(x) & P_B(z).

Правило LS2’. P(x, z) & Q(x, z, u) & Q_A(x, y) & Q_B(z, t)├ P_C(y, t) & Q_C(y, t, u).

Предполагая однозначность предикатов A и B, а также их спецификаций, проведем эквивалентные преобразования LS1’ и LS2’, устраняя переменные y и t. Получим следующие правила.

Правило LS8. P(x, z) ├ P_A(x) & P_B(z).

Правило LS9. P(x, z) & Q(x, z, u)├ P_C(A(x), B(z)) & Q_C(A(x), B(z), u).

Справедлива следующая лемма.

Лемма 5.8. Допустим, спецификация P(x, z) и Q(x, z, u) оператора (5.15) реализуема, операторы A, B и C однозначны в области предусловий и корректны, а их спецификации однозначны. Если правила LS8 и LS9 истинны, то оператор (5.15) является корректным.

Нетрудно проверить, что леммы 5.7 и 5.8 верны для любого числа вызовов, используемых в качестве аргументов вызова предиката C, в том числе и для одного вызова.

Пусть имеется оператор суперпозиции z = a * b; y = z + c. Как определено выше, операции a * b и z + c являются аналогами вызовов предикатов *(a, b: z) и +(*z, c: y). Применим схему подстановки вызова на место аргумента во втором вызове суперпозиции. Подстановка a * b на место z в операторе y = z + c дает оператор y = (a * b) + c. Здесь используется правило: подставляемая операция на место аргумента другой операции обрамляется круглыми скобками. Таким образом, приходим к известному понятию выражения. Использование правил приоритетов операций, позволяющих опускать круглые скобки, определяет привычную форму записи выражений; например, y = a * b + c.

Переменные, изображения констант, вызовы функций и их представление в виде операций являются частными случаями понятия выражения. Таким образом, в языке P3 позиция аргумента вызова в общем случае содержит выражение.

Имеет место тождество

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

Учитывая это, в языке P3 в позиции (b) условного оператора будем использовать произвольное выражение логического типа.

Язык CCP определен как бестиповый язык. При этом тип каждой переменной программы на языке CCP можно распознать, используя информацию о вхождениях переменной в программе. Язык P также можно реализовать как бестиповый подобно языку Лисп. Однако в случае использования полиморфных операций, например «+», можно привести примеры программ, когда невозможно однозначно определить типы переменных, что предопределяет неоднозначность программы. Тем не менее, и при использовании полиморфных операций можно было бы построить бестиповый язык, введя соответствующие ограничения. Язык P определен как типовый. Описания аргументов и результатов предикатов и локальных переменных снабжаются указанием типов в стиле языка C. Тип, математическое описание которого дается в разд. 4.2, кодируется в языке P конструкцией ИЗОБРАЖЕНИЕ-ТИПА; см. разд. 6.7. Аргументация в пользу типового языка заключается в том, что указание типов переменных существенно повышает понимание программы.