ФЕДЕРАЛЬНОЕ АГЕНТСТВО ПО ОБРАЗОВАНИЮ
НОВОСИБИРСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ
Факультет информационных технологий
В. И. ШЕЛЕХОВ
Предикатное программирование
Учебное пособие
Оглавление
Введение в курс предикатного программирования .............................................................. 5
1. Общее понятие программы ........................................................................................... 6
1.1. Автоматическая вычислимость ....................................................................................... 6
1.2. Спецификация программы .............................................................................................. 7
1.3. Формы спецификации программы .................................................................................. 9
Список литературы ................................................................................................................. 10
2. Корректность программ с предикатной спецификацией ................................... 12
2.1. Предикатная спецификация программы ...................................................................... 12
2.2. Логическая семантика языка программирования ....................................................... 13
2.3. Модель корректности программы ................................................................................ 15
2.4. Система правил доказательства корректности операторов ........................................ 16
2.4.1. Правила для корректного оператора .................................................................. 17
2.4.2. Правила корректности для параллельного оператора ...................................... 17
2.4.3. Правила корректности для оператора суперпозиции ....................................... 17
2.4.4. Правила корректности для условного оператора .............................................. 18
2.5. Система правил вывода программы из спецификации ............................................... 19
2.5.1. Однозначность предикатов ................................................................................. 19
2.5.2. Теорема тождества спецификации и программы .............................................. 19
2.5.3. Правила корректности для параллельного оператора ...................................... 20
2.5.4. Правила корректности для оператора суперпозиции ....................................... 21
2.5.5. Правила корректности для условного оператора .............................................. 22
2.6. Заключение .............................................................................................................. 22
Список литературы ................................................................................................................. 23
3. Математические основы ........................................................................................... 24
3.1. Отношения порядка ....................................................................................................... 24
3.2. Наименьшая неподвижная точка .................................................................................. 25
3.3. Математическая индукция ............................................................................................ 25
Список литературы ................................................................................................................. 26
Введение .......................................................................................................................... 58
Лексемы .......................................................................................................................... 59
Предикаты ....................................................................................................................... 60
6.3.1. Определение предиката ....................................................................................... 60
6.3.2. Спецификация предиката .................................................................................... 62
6.3.3. Вызов предиката ................................................................................................... 62
Программа ....................................................................................................................... 64
Операторы ....................................................................................................................... 65
Выражения ...................................................................................................................... 67
Типы ................................................................................................................................. 70
Массивы .......................................................................................................................... 75
6.8.1. Описание типа массива ....................................................................................... 75
6.8.2. Вырезка массива ................................................................................................... 76
6.8.3. Определениеи массива ......................................................................................... 76
6.8.4. Объединение массивов ........................................................................................ 77
Формулы .......................................................................................................................... 78
Процессы ......................................................................................................................... 79
Императивное расширение .......................................................................................... 82
Список литературы ................................................................................................................. 83
7. Технология предикатного программирования .................................................... 84
7.1. Подстановка определения предиката на место вызова ............................................... 84
7.2. Замена хвостовой рекурсии циклом ............................................................................. 86
7.3. Склеивание переменных ................................................................................................ 87
7.4. Метод обобщения исходной задачи ............................................................................. 88
7.5. Трансформация кодирования структурных объектов ................................................ 89
7.6. Пример. Сортировка простыми вставками .................................................................. 91
7.7. Гиперфункции ............................................................................................................... 96
7.8. Заключение ................................................................................................................... 108
Список литературы ............................................................................................................... 109
Введение в курс предикатного программирования
В представленном учебнике изложен материал лекций по предикатному программированию, которые читались в Новосибирском государственном университете с 2006 по 2009 гг. Данный курс имел два названия: «Формальные методы в описании языков и систем программирования» для студентов 2-го курса магистратуры факультета информационных технологий и «Предикатное программирование» для студентов механико-математического факультета.
Курс начинается общеметодологическим определением понятия программы с рассмотрением двух основных свойств программы: автоматической вычислимости и наличия спецификации. Во втором разделе излагается модель корректности программ для функциональных и императивных программ. Определяется понятие спецификации программы в форме тройки Хоара. Вводится понятие логической семантики. Определяются две системы правил доказательства корректности для оператора суперпозиции, параллельного оператора и условного оператора. В третьем разделе излагаются отдельные положения математической логики: отношения порядка, наименьшая неподвижная точка и метод полной структурной математической индукции. Четвертый раздел описывает язык исчисления вычислимых предикатов CCP (Calculus of Computable Predicates) и его формальную (логическую и операционную) семантику. Для всех конструкций языка и программы в целом доказывается согласованность логической и операционной семантики. Рекурсивные определения предикатов трактуются с использованием аппарата наименьшей неподвижной точки. Язык CCP определяется как минимальное ядро, из которого можно построить любой чистый язык функционального программирования; при этом семантика языка выражается через семантику конструкций ядра. В пятом разделе определяется расширяющаяся цепочка языков CCP Ì P1 Ì P2 Ì P3. Язык P1 получается из CCP применением открытой подстановки определений предикатов на место их вызовов. В языке P2 определяются обобщенные формы оператора суперпозиции и параллельного оператора. Язык P3 определяет набор конструкций, которые в языках императивного программирования соответствуют понятию выражения. Для языков P2 и P3 определяется система правил доказательства корректности новых языковых конструкций. Правила доказательства корректности рекурсивных предикатов определяются в виде правил структурной полной математической индукции.
В шестом разделе в полном объеме описывается последняя версия языка предикатного программирования, оформленная в стиле серии языков C, C++ и др., привычном для подавляющего большинства программистов. В седьмом разделе описываются технология предикатного программирования и методы доказательства корректности предикатных программ. Представлен метод управляемой полуавтоматической трансляции применением последовательности трансформаций, преобразующих предикатную программу в эффективную императивную программу на императивном расширении языка P. Используются трансформации четырех видов: склеивание переменных, реализующее замену нескольких переменных одной; замена хвостовой рекурсии циклом; подстановка определения предиката на место его вызова; кодирование структурных объектов низкоуровневыми структурами с использованием массивов и указателей. Описывается универсальный метод обобщения исходной задачи для получения решения с хвостовой формой рекурсии. Этот метод нередко оказывается ключевым для эффективной реализации предикатных программ. Предлагается языковая конструкция нового вида - гиперфункция, позволяющая гибко декомпозировать программу произвольным образом.
Список литературы
1. Программа // Краткая российская энциклопедия. М.: Большая российская энциклопедия ОНИКС 21 век, 2003.
2. Марков А. А., Нагорный Н.М. Теория алгорифмов. М.: Наука, Физматлит, 1984. - 432 с.
3. Минский М. Вычисления и автоматы: Пер. с англ. М.: Мир, 1971. - 364 с.
4. Питерсон Дж. Теория сетей Петри и моделирование систем. М.: Мир, 1984. - 264 с.
5. Gosling J., Joy B., Steele G. The Java Language Specification. Pre-Release Version 1.0, Draft 5.2 - July 3, 1996.
6. Kain R. Y. Automata Theory: Machines and Languages. - McGraw-Hill, N. Y., 1972. - 301 p.
7. Gurevich Y. Sequential Abstract State Machines capture Sequential Algorithms // ACM Transactions on Computational Logic. - 2000. - Vol. 1, N 1. - P. 77-111.
8. Шелехов В. И. Инвариант языка программирования // Средства и инструменты окружений программирования. - Новосибирск, 1995. - С. 6-22.
9. Мир Лиспа: Пер. с англ. М.: Мир, 1990. Т. 2. Методы и системы программирования. - 318 с.
10. Клини С. К. Введение в метаматематику, пер. с англ., М., 1957.
11. Ершов А .П., Шура-Бура М. Р. Пути развития программирования в СССР. - Новосибирск, 1976. (Препринт ВЦ СО АН СССР, №12)
12. Hoare C. A. R. Communicating Sequential Processes. Prentice-Hall, 1985.
13. Watt D.A. Programming Language Concepts and Paradigms. Prentice Hall, 1990. - 322 p.
14. Лавров С.С. Программирование. Математические основы, средства, теория. - СПб: БХВ-Петербург, 3001. - 320 с.
15. Meyer B. Introduction to the Theory of Programming Languages. Prentice Hall, 1990. - 448 p.
16. Zamulin A. V. Algebraic Semantics of an Imperative Programming Language as a Compiler Abstract Model // Joint NCC&ISS Bull., 20. - Comp. Science, 2004. - P. 113-128.
17. Замулин А. В. Алгебраическая семантика императивного языка программирования // Программирование. 2003, № 6. - С. 1-14.
Система правил доказательства корректности операторов
Понятие корректности, введенное для программы в целом, применимо также к произвольным операторам программы. Допустим, для некоторого оператора S имеется спецификация в виде тройки Хоара {P(x)} S {Q(x, y)}. В качестве оператора S будем рассматривать оператор суперпозиции A; B, параллельный оператор A || B или условный оператор if (C) A elseB, определенные в разд. 2.2. Нашей задачей является конкретизация формулы корректности (2.10) для каждого из трех операторов. Естественным требованием является корректность операторов A и B. Условия корректности каждого из трех операторов формулируются в виде правил вывода, с помощью которых можно доказывать корректность оператора. Правила вывода для этих операторов не используют формулы LS(A) и LS(B) - только спецификации (предусловия и постусловия) операторов A и B встречаются в правилах. Эта особенность является существенным преимуществом правил.
Правила для корректного оператора
Для произвольного корректного оператора B перепишем условия корректности (2.7-2.9) в виде правил вывода.
Лемма 2.3. Пусть имеется оператор B со спецификацией в виде тройки Хоара {PB(x)} B {QB(x, y)}. Предполагается, что оператор B является корректным, т. е. для него истинна соответствующая общая формула корректности (2.10) и формулы (2.7-2.9). Тогда истинны следующие правила вывода.
Правило E1. PB(x) ├ $y. QB(x, y).
Правило E2. PB(x) ├ $y. LS(B)(x, y).
Правило E3. PB(x) ├ LS(B)(x, y) Þ QB(x, y).
Правила корректности для параллельного оператора
Рассмотрим спецификацию параллельного оператора в виде тройки Хоара:
{P(x)} A || B {Q(x, y, z)} . (2.11)
Допустим, операторы A и B корректны. Их спецификации представлены тройками:
{PA(x)} A {QA(x, y)}, {PB(x)} B {QB(x, z)} .
Определим правила, гарантирующие корректность параллельного оператора.
Правило RP1. P(x) ├ PA(x) & PB(x).
Правило RP2. QA(x, y), QB(x, z) ├ Q(x, y, z).
Лемма 2.4. Пусть предусловие P(x) истинно. Допустим, операторы A и B корректны. Если правила RP1 и RP2 истинны (т. е. правая часть доказуема из левой части для каждого правила), то параллельный оператор (2.11) является корректным.
Доказательство. Для доказательства корректности оператора (2.11) в соответствии с формулой (2.10) достаточно доказать реализуемость LS(A || B)(x, y, z) и выводимость постусловия Q(x, y, z) из LS(A || B)(x, y, z). В соответствии с (2.2) формула LS(A || B)(x, y, z) эквивалентна формуле LS(A)(x, y) & LS(B)(x, z).
Из истинности предусловия P(x) по правилу RP1 следует истинность PA(x) и PB(x). Далее, по правилу E2 становятся истинными формулы $y. LS(A)(x, y) и $z. LS(B)(x, z). Их конъюнкция определяет реализуемость LS(A || B)(x, y, z).
Докажем выводимость постусловия Q(x, y, z) из LS(A)(x, y) & LS(B)(x, z). Допустим, истинна формула LS(A)(x, y) & LS(B)(x, z). Применим правило E3 для PA(x) и PB(x), истинность которых определена выше. Получаем истинность формул LS(A)(x, y) Þ QA(x, y) и LS(B)(x, z) Þ QB(x, z). Как следствие, будут истинны QA(x, y) и QB(x, z). Применяя правило RP2, получаем истинность постусловия Q(x, y, z). □
Правила корректности для оператора суперпозиции
Рассмотрим спецификацию оператора суперпозиции в виде тройки Хоара:
{P(x)} A; B {Q(x, y)} . (2.12)
Предположим, что операторы A и B корректны. Их спецификации представлены тройками:
{PA(x)} A {QA(x, z)}, {PB(z)} B {QB(z, y)} .
Определим правила, гарантирующие корректность оператора суперпозиции (2.12).
Правило RS1. P(x) ├ PA(x) & "z (QA(x, z) Þ PB(z)).
Правило RS2. P(x) & $z (QA(x, z) & QB(z, y)) ├ Q(x, y).
Лемма 2.5. Пусть предусловие P(x) истинно. Допустим, операторы A и B корректны. Если правила RS1 и RS2 истинны, то оператор суперпозиции (2.12) является корректным.
Доказательство. В соответствии с формулой (2.10) достаточно доказать реализуемость LS(A; B)(x, y) и выводимость постусловия Q(x, y) из LS(A; B)(x, y). В соответствии с (2.1) формула LS(A; B)(x, y) определена как $z.(LS(A)(x, z) & LS(B)(z, y)).
Из истинности предусловия P(x) по правилу RS1 следует истинность формул PA(x) и "z (QA(x, z) Þ PB(z)). Из истинности PA(x) и правила E2 следует истинность формулы $z. LS(A)(x, z). Допустим, для некоторого z0 формула LS(A)(x, z0) истинна. Из истинности PA(x) и правила E3 следует истинность LS(A)(x, z0) Þ QA(x, z0). Как следствие, истинно QA(x, z0). Далее, из истинности формулы "z (QA(x, z) Þ PB(z)) следует истинность PB(z0). По правилу E2 истинна формула $y LS(B)(z0, y). Далее, истинна конъюнкция LS(A)(x, z0) & $y LS(B)(z0, y), и затем – формула $y. $z. (LS(A)(x, z) & LS(B)(z, y)), т. е. доказана реализуемость LS(A; B)(x, y).
Докажем выводимость постусловия Q(x, y) из LS(A; B)(x, y). Пусть LS(A; B)(x, y) истинно, т. е. истинна формула $z.(LS(A)(x, z) & LS(B)(z, y)). Пусть формула истинна для некоторого z1. По правилу E3 истинна формула LS(A)(x, z1) Þ QA(x, z1) и далее – QA(x, z1). Истинность QA(x, z1) и "z (QA(x, z) Þ PB(z)) влечет истинность PB(z1). По правилу E3 истинно LS(B)(z1, y) Þ QB(z1, y). Поскольку LS(B)(z1, y) истинно, то истинно QB(z1, y). Таким образом, истинна правая часть правила RS2, а значит – и левая, т. е. истинно постусловие Q(x, y). □
Правила корректности для условного оператора
Рассмотрим спецификацию условного оператора в виде тройки Хоара:
{P(x)} if (C) A elseB {Q(x, y)} . (2.13)
Предположим, что операторы A и B корректны. Их спецификации представлены тройками:
{PA(x)} A {QA(x, y)} , {PB(x)} B {QB(x, y)} .
Определим правила, гарантирующие корректность условного оператора (2.13).
Правило RC1. P(x) & C ├ PA(x).
Правило RC2. P(x) & ØC ├ PB(x).
Правило RC3. P(x) & C & QA(x, y) ├ Q(x, y).
Правило RC4. P(x) & ØC & QB(x, y) ├ Q(x, y).
Отметим, что условие C зависит от x.
Лемма 2.6. Пусть предусловие P(x) истинно. Допустим, операторы A и B корректны. Если правила RC1, RC2, RC3 и RC4 истинны, то условный оператор (2.13) является корректным.
Доказательство. Для оператора (2.13) необходимо доказать формулу (2.10). В ней дважды встречается подформула LS(if (C) A elseB)(x, y), определяемая согласно (3) в виде:
(C Þ LS(A)(x, y)) & (ØC Þ LS(B)(x, y)) . (2.14)
В соответствии с формулой (2.10) достаточно доказать реализуемость формулы (2.14) и выводимость постусловия Q(x, y) из (2.14).
Допустим, что условие C истинно. Из истинности предусловия P(x) по правилу RC1 следует истинность PA(x). По правилу E2 истинна формула $y. LS(A)(x, y). Далее будет истинной формула $y. (C Þ LS(A)(x, y)). Из истинности C следует истинность формулы ØC Þ LS(B)(x, y) и, следовательно, формулы $y. [(C Þ LS(A)(x, y)) & (ØC Þ LS(B)(x, y))]. Это обеспечивает реализуемость формулы (2.14) в случае истинности C. Реализуемость (2.14) в случае ложности C доказывается аналогичным образом.
Докажем выводимость постусловия Q(x, y) из формулы (2.14). Допустим, истинна формула (2.14). Пусть C истинно. Тогда истинно LS(A)(x, y). По правилу RC1 истинно PA(x). По правилу E3 истинна формула LS(A)(x, y) Þ QA(x, y), а значит – и QA(x, y). Таким образом, истинна правая часть правила RC3. Тогда истинна левая часть правила, т. е. истинно постусловие Q(x, y). Доказательство истинности постусловия Q(x, y) для случая, когда C ложно, проводится аналогично с использованием правила RC4. □
Правила корректности для параллельного оператора
Рассмотрим спецификацию параллельного оператора в виде тройки Хоара:
{P(x)} A || B {Q(x, y, z)} [8] . (2.17)
Допустим, операторы A и B корректны. Их спецификации представлены тройками:
{PA(x)} A {QA(x, y)} , {PB(x)} B {QB(x, z)} .
Определим правила, гарантирующие корректность параллельного оператора.
Правило LP1. P(x) ├ PA(x) & PB(x).
Правило LP2. P(x) & Q(x, y, z) ├ QA(x, y).
Правило LP3. P(x) & Q(x, y, z) ├ QB(x, z).
Лемма 2.10. Допустим, спецификация параллельного оператора (2.17) реализуема, операторы A и B однозначны в области предусловий и корректны, а их спецификации - однозначны. Если правила LP1, LP2 и LP3 истинны (т. е. правая часть доказуема из левой части для каждого правила), то параллельный оператор (2.17) является корректным.
Доказательство. Поскольку операторы A и B однозначны, то и параллельный оператор (2.17) является однозначным. Поскольку спецификация оператора (2.17) реализуема, в соответствии с теоремой 2.1 для доказательства леммы достаточно доказать истинность формулы:
P(x) & Q(x, y, z) Þ LS(A || B)(x, y, z) .
В соответствии с (2.2) формула LS(A || B)(x, y, z) эквивалентна LS(A)(x, y) & LS(B)(x, z).
Пусть истинны P(x) и Q(x, y, z). Докажем истинность LS(A)(x, y) и LS(B)(x, z). Из истинности предусловия P(x) по правилу LP1 следует истинность PA(x) и PB(x). По правилам LP2 и LP3 становятся истинными QA(x, y) и QB(x, z). Для предикатов A и B выполняются условия леммы 2.9. Поэтому истинны формулы:
PA(x) & QA(x, y) Þ LS(A)(x, y);
PB(x) & QB(x, z) Þ LS(B)(x, z).
Поскольку посылки этих формул истинны, то истинны LS(A)(x, y) и LS(B)(x, z). □
Правила корректности для оператора суперпозиции
Рассмотрим спецификацию оператора суперпозиции в виде тройки Хоара:
{P(x)} A; B {Q(x, y)} [9] . (2.18)
Предположим, что операторы A и B корректны. Их спецификации представлены тройками:
{PA(x)} A {QA(x, z)} , {PB(z)} B {QB(z, y)} .
Определим правила, гарантирующие корректность оператора суперпозиции (2.18).
Правило LS1. P(x) ├ PA(x).
Правило LS2. P(x) & Q(x, y) & QA(x, z) ├ PB(z) & QB(z, y).
Лемма 2.11. Допустим, спецификация оператора суперпозиции (2.18) реализуема, операторы A и B однозначны в области предусловий и корректны, а их спецификация B однозначна. Если правила LS1 и LS2 истинны, то оператор суперпозиции (2.18) является корректным.
Доказательство. Поскольку операторы A и B однозначны, то и оператор суперпозиции (2.18) является однозначным. В соответствии с теоремой 2.1 для доказательства леммы достаточно доказать истинность формулы:
P(x) & Q(x, y) Þ LS(A; B)(x, y) .
В соответствии с (2.1) формула LS(A; B)(x, y) эквивалентна $z.(LS(A)(x, z) & LS(B)(z, y)).
Пусть истинны P(x) и Q(x, y). Докажем истинность $z.(LS(A)(x, z) & LS(B)(z, y)). Из истинности предусловия P(x) по правилу LS1 следует истинность PA(x). Из корректности оператора A следует истинность формул $z. LS(A)(x, z) и LS(A)(x, z) Þ QA(x, z). Допустим для некоторого z0 истинно LS(A)(x, z0). Тогда истинно QA(x, z0). В соответствии с правилом LS2 истинна формула PB(z0) & QB(z0, y). В соответствии с леммой 2.9 истинна формула
PB(z) & QB(z, y) Þ LS(B)(z, y) .
Тогда истинна LS(B)(z0, y). В итоге, будет истинна формула $z.(LS(A)(x, z) & LS(B)(z, y)). □
Правила корректности для условного оператора
Рассмотрим спецификацию условного оператора в виде тройки Хоара:
{P(x)} if (C) A elseB {Q(x, y)} [10] . (2.19)
Предположим, что операторы A и B корректны. Их спецификации представлены тройками:
{PA(x)} A {QA(x, y)} , {PB(x)} B {QB(x, y)} .
Определим правила, гарантирующие корректность условного оператора (2.19).
Правило LC1. P(x) & Q(x, y) & C ├ PA(x) & QA(x, y).
Правило LC2. P(x) & Q(x, y) & ØC ├ PB(x) & QB(x, y).
Лемма 2.12. Допустим, спецификация условного оператора (2.19) реализуема, операторы A и B однозначны в области предусловий и корректны, а их спецификации однозначны. Если правила LC1 и LC2 истинны, то условный оператор (2.19) является корректным.
Доказательство. Поскольку операторы A и B однозначны, то и условный оператор (2.19) является однозначным. В соответствии с теоремой 2.1 для доказательства леммы достаточно доказать истинность формулы:
P(x) & Q(x, y) Þ LS(if (C) A elseB)(x, y) .
В соответствии с (2.3) формула LS(if (C) A elseB)(x, y) эквивалентна
(C Þ LS(A)(x, y)) & (ØC Þ LS(B)(x, y)) .
Пусть истинны P(x) и Q(x, y). Докажем истинность формулы C Þ LS(A)(x, y). Пусть истинно C. Докажем истинность LS(A)(x, y). Можно применить правило LC1, поскольку истинны P(x), Q(x, y) и C. Получим истинность формулы PA(x) & QA(x, y). В соответствии с леммой 2.9 истинна формула
PA(x) & QA(x, y) Þ LS(A)(x, y) .
Поскольку истинна посылка, то истинно LS(A)(x, y). Следовательно, доказана истинность формулы C Þ LS(A)(x, y). Истинность формулы ØC Þ LS(B)(x, y) доказывается аналогично. □
Заключение
Корректность программы определяется для класса программ с предикатной спецификацией и для языков с логической семантикой. Представленную модель корректности естественно рассматривать как развитие модели Хоара [9]. Использование свойств логической семантики позволяет определить корректность программы в виде явной логической формулы (2.10), в которой программа S представлена логическим эквивалентом LS(S). В случае, когда оператор S является однозначным, а спецификация реализуема и однозначна, можно использовать формулу корректности (2.16) в соответствии с теоремой тождества спецификации и программы.
Важнейшей особенностью всех правил доказательства корректности является то, что они не используют формул LS(A) и LS(B) - только спецификации (предусловия и постусловия) операторов A и B встречаются в правилах. Это определяет универсальную применимость правил для любых языков программирования, в том числе императивных, для которых проблематично построить логическую семантику - для применимости достаточно того, чтобы программная композиция пары операторов A и B по форме соответствовала одному из указанных трех операторов языка CCP.
Системы правил доказательства корректности определяют алгоритм доказательства корректности программ. Данный алгоритм можно использовать для реализации системы автоматической верификации корректности. Эта система будет существенно более эффективной по сравнению с системой верификации, построенной с использованием формул (2.10) и (2.16). Алгоритм доказательства корректности можно также использовать как метод доказательства «вручную», т. е. в традиционном математическом стиле. Этот метод применялся для доказательства корректности нетривиального алгоритма МакКрейта построения дерева суффиксов [6].
Отсутствие операторов цикла в рассматриваемом наборе операторов не позволяет полноценно показать новую технику доказательства корректности на примерах программ. Аналогами циклов в языке CCP являются рекурсивные определения предикатов. Доказательство корректности рекурсивно определяемых предикатов реализуется с применением структурной и полной индукции [2]; см. гл. 3.
Язык CCP может быть использован в качестве ядра при построении любого чистого языка функционального программирования в виде иерархической системы обозначений. Например, рассмотрим обобщенный оператор суперпозиции A; B для операторов вида A: x®z, r и B: z, x®p, где x, z, r и p обозначают разные наборы переменных, причем наборы x и r могут быть пустыми. Обобщенный оператор A; B может быть определен в виде композиции простого оператора суперпозиции и параллельного оператора. При этом правила доказательства корректности для обобщенного оператора суперпозиции нетрудно получить из соответствующих правил для простого оператора суперпозиции и параллельного оператора.
Список литературы
1. Дейкстра Э. Дисциплина программирования: Пер. с англ. М.: Мир, 1978. 272 с.
2. Шелехов В. И. Модель корректности программ на языке исчисления вычислимых предикатов. Новосибирск, 2007. 51 с. (Препр. / ИСИ СО РАН; № 145).
3. Шелехов В. И. Исчисление вычислимых предикатов. Новосибирск, 2007. 24 с. (Препр. / ИСИ СО РАН; № 143).
4. Шелехов В. И. Анализ общего понятия программы // Методы предикатного программирования. Новосибирск, 2006. Вып. 2. C. 7–16.
5. Шелехов В. И. Язык спецификации процессов // Методы предикатного программирования. Вып.2. Новосибирск, 2006. C. 17–34.
6. Шелехов В. И. Разработка программы построения дерева суффиксов в технологии предикатного программирования. Новосибирск, 2004. 52 с. (Препр. / ИСИ СО РАН; № 115).
7. Шелехов В. И. Введение в предикатное программирование. Новосибирск, 2002. 82 с. (Препр. / ИСИ СО РАН; № 100).
8. Scott D. S. and Strachey C. Towards a mathematical semantics for computer languages // Computers and Automata. 1971. P. 19–46.
9. Hoare C. A. R. An axiomatic basis for computer programming // Communications of the ACM. 1969. Vol. 12 (10). P. 576–585.
10. Floyd R. W. Assigning meanings to programs // Proceedings Symposium in Applied Mathematics, Mathematical Aspects of Computer Science. AMS, 1967. P. 19–32.
11. McCarthy J. A basis for a mathematical theory of computation // Computer Programming and Formal Systems. 1963. P. 33–70.
12. Milner R. A. Calculus of Communicating Systems // Lecture Notes in Computer Science, 1980. Vol. 92.
13. Hoare C. A. R. Communicating Sequential Processes. Prentice-Hall. 1985.
14. Andrews J. H. A logical semantics for depth-first Prolog with ground negation // Theoretical computer science. 1997. Val. 184. P. 105–143.
15. Hehner E. C. R. A Practical Theory of Programming, 2nd edition. 2004; URL: http://www.cs.toronto.edu/~hehner/aPToP/
16. Автоматизированный реинжиниринг программ / Под ред. проф. А. Н. Терехова и А. А. Терехова. СПб.: Изд-во С.-Петерб. ун-та, 2000. 332 с.
17. 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.
Математические основы
В данном разделе собраны известные математические понятия, используемые в дальнейшем изложении.
Список литературы
1. Гончаров С. С. Математическая логика: Учеб. пособие. Новосибирск, 2007. 166 с.
2. Hopcroft J. E., Motwani R., Ullman J. D. Introduction to Automata Theory, Languages, and Computation, 2nd ed. Addison Wesley, 2001. 521 p.
3. Кнут Д. Искусство программирования для ЭВМ. М.: Мир, 1976. Т. 1. С. 38–50.
4. Клини С. К. Введение в метаматематику: Пер. с англ. М.: 1957. 526 с.
5. Mathematical induction. URL: http://en.wikipedia.org/wiki/Mathematical_induction.
Язык исчисления вычислимых предикатов,
Оператор суперпозиции
Оператор суперпозиции является правой частью следующего определения предиката:
A(x: y) º B(x: z); C(z: y) . (4.16)
Здесь x, y и z - произвольные непересекающиеся наборы переменных, причем набор x может быть пустым. Если B или C есть имя переменной предикатного типа, оно входит в набор x. Переменные набора z являются локальными переменными. Логическая семантика оператора суперпозиции представлена следующим образом:
LS(B(x: z); C(z: y)) @ $z. (B(x, z) & C(z, y)) . (4.17)
Допустим, определение предиката A исполняется в рамках секции s. Секция s состоит из переменных наборов x, y и z. Исполнение правой части определения (4.16) соответствует оператору runStat(s, K(x:y)) в (4.14) и определяется следующим образом:
runCall(s, B(x: z)); (4.18)
runCall(s, C(z: y)) .
Таким образом, алгоритм вычисления суперпозиции состоит в последовательном исполнении вызовов предикатов B и C. Значения переменных набора z, вычисленные при исполнении предиката B, используются при вычислении предиката C.
Лемма 4.3. Cons(B) & Cons(C) Þ Cons(H), где H обозначает B(x: z); C(z: y).
Доказательство. Пусть истинно Cons(B) и Cons(C). Докажем истинность Cons(H). Зафиксируем значения x и y. Пусть истинна H(x:y), т. е. истинна правая часть (4.17). Для некоторого z будут истинны B(x: z) и C(z: y). Из Cons(B) и Cons(C) следует, что исполнение B(x: z) завершается получением набора z, а исполнение C(z: y) - вычислением набора y. Поэтому исполнение операторов (4.18), а значит и H(x:y), завершается вычислением y. Это доказывает первую часть истинности Cons(H).
Допустим, исполнение H(x: y) завершается вычислением y. Докажем истинность H(x:y). Исполнение пары операторов (4.18) завершается вычислением y. В частности, завершается первый оператор runCall(s, B(x: z)). Тогда существует некоторый набор z, являющийся результатом исполнения. Таким образом, для некоторого z исполняются вызовы B(x: z) и C(z: y). Из Cons(B) и Cons(C) следует истинность B(x: z) и C(z: y). Следовательно, истинна правая часть (18) и H(x: y). □
Параллельный оператор
Параллельный оператор является правой частью следующего определения предиката:
A(x: y, z) º B(x: y) || C(x: z) . (4.19)
Здесь, x, y и z - произвольные непересекающиеся наборы переменных, причем набор x может быть пустым. Если B или C есть имя переменной предикатного типа, то оно входит в набор x. Логическая семантика параллельного оператора представлена следующим образом:
LS(B(x: y) || C(x: z)) @ B(x, y) & C(x, z) .
Допустим, определение предиката A исполняется в рамках секции s. Секция s состоит из переменных наборов x, y и z. Исполнение правой части определения (4.19) соответствует оператору runStat(s, K(x:y)) в (4.14) и определяется следующим образом:
runCall(s, B(x: y)) ||
runCall(s, C(x: z)) .
Алгоритм вычисления параллельной композиции || на метаязыке слагается из независимого вычисления указанных вызовов предикатов B и C. Поскольку эти два вычисления между собой не взаимодействуют, они могут проводиться параллельно. Эффект параллельной композиции равен конъюнкции эффектов композируемых операторов, т. е. B(x, y) & C(x, z).
Лемма 4.4. Cons(B) & Cons(C) Þ Cons(H), где H обозначает B(x: y) || C(x: z).
Условный оператор
Условный оператор является правой частью следующего определения предиката:
A(b, x: y) º if (b) B(x: y) elseC(x: y) . (4.20)
Здесь x и y - произвольные непересекающиеся наборы переменных, причем набор x может быть пустым, b - переменная логического типа, не встречающаяся в наборах x и y. Если B или C есть имя переменной предикатного типа, то оно входит в набор x. Логическая семантика условного оператора представлена следующим образом:
LS(if (b) B(x: y) elseC(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)) elserunCall(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) elseC(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 проводится аналогично. □
Список литературы
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 оператор суперпозиции и параллельный оператор общего вида: A1(…); A2(…); … ; An(…) и A1(…) ½½ A2(…) ½½ … ½½ An(…) для n > 1.
Рассмотрим оператор суперпозиции общего вида со спецификацией в виде предусловия P(x) и постусловия Q(x, y):
P(x) {B1(x: z1); B2(z1: z2) ;...; Bj(zj-1: zj) ;...; Bn(zn-1: y)} Q(x, y) [18] . (5.3)
Здесь x, z1, z2, …, zn-1, y - различные непересекающиеся наборы переменных; B1, B2, …, Bn обозначают вызовы предикатов или блоки языка P1 со спецификациями (предусловиями и постусловиями) PB1(x), QB1(x, z1), PB2(z1), QB2(z1, z2), …, PBn(zn-1), QBn(zn-1, y). Логическая семантика оператора суперпозиции общего вида определяется на основе логической семантики суперпозиции двух операторов (4.17):
LS(B1(x: z1); B2(z1: z2) ;...; Bj(zj-1: zj) ;...; Bn(zn-1: y)) º
$z1,z2,...,zn-1. LS(B1(x: z1)) & LS(B2(z1: z2)) &...& LS(Bj(zj-1: zj)) &...& LS(Bn(zn-1: y)) . (5.4)
Допустим, определение предиката A исполняется в рамках секции s. Секция s состоит из переменных наборов x, y и z1, z2, ..., zn-1. Исполнение оператора (5.3) реализуется на метаязыке оператором runStat(s, B1(x: z1); …; Bn(zn-1: y)) в (4.14) и определяется следующим образом:
runCallBlock(s, B1(x: z1)); (5.5)
runCallBlock(s, B2(z1: z2)); .....;
runCallBlock(s, Bj(zj-1: zj)); .....;
runCallBlock(s, Bn(zn-1: y)) .
Здесь runCallBlock обозначает runCall, если вторым параметром является вызов предиката, или runBlock в случае блока.
Определим правила серии L, гарантирующие корректность оператора суперпозиции общего вида (5.3).
Правило LS3. P(x) ├ PB1(x).
Правило LS4. P(x) & Q(x, y) & QB1(x, z1) ├
$!z2,z3,...,zn-1. PB2(z1) & QB2(z1, z2) &...& PBj(zj-1) & QBj(zj-1, zj) &...& PBn(zn-1) & QBn(zn-1, y).
Лемма 5.1. Допустим, спецификация P(x) и Q(x, y) оператора суперпозиции общего вида реализуема, операторы B1, …, Bn однозначны в области предусловий и корректны, а их спецификации однозначны. Если правила LS3 и LS4 истинны, то оператор суперпозиции (5.3) является корректным.
Доказательство. Поскольку операторы B1, …, Bn однозначны, то и оператор суперпозиции (5.3) является однозначным. В соответствии с (5.4) и теоремой 2.1 для доказательства леммы достаточно доказать истинность формулы
P(x) & Q(x, y) Þ
$z1,z2,...,zn-1. LS(B1(x: z1)) & LS(B2(z1: z2)) &...& LS(Bj(zj-1: zj)) &...& LS(Bn(zn-1: y)) . (5.6)
Пусть истинны P(x) и Q(x, y). Докажем истинность правой части (5.6). Из истинности предусловия P(x) по правилу LS3 следует истинность PB1(x). Из корректности оператора B1 по правилу E2 следует истинность формулы $z1. LS(B1(x: z1)). Допустим, для некоторого z’1 истинно LS(B1(x: z’1)). Для оператора B1 истинны условия леммы 2.8. Поэтому истинно QB1(x, z’1). В соответствии с правилом LS4 истинна правая часть LS4 для z1 = z’1. Тогда из истинности PBj(zj-1) & QBj(zj-1, zj) для j = 3,…, n (zn = y) по лемме 2.9 следует истинность LS(Bj(zj-1: zj)). Это доказывает истинность формулы (5.6). □
Определим правила серии R, гарантирующие корректность оператора суперпозиции общего вида (5.3).
Правило RS3. P(x) ├ PB1(x) & "z1,z2,..., zn-1.
(QB1(x, z1) Þ PB2(z1)) & (QB2(z1, z2) Þ PB3(z2)) & ... & (QBn-1(zn-2, zn-1) Þ PBn(zn-1)).
Правило RS4. P(x) & $z1,z2,...,zn-1 (QB1(x, z1) & QB2(z1, z2) & ... & QBn(zn-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 следует истинность правой части правила, в том числе формулы PB1(x). Из истинности PB1(x) и правила E2 следует истинность формулы $z. LS(B1(x: z)). Допустим, для некоторого z’1 формула LS(B1(x: z’1)) истинна. Из истинности PB1(x) и правила E3 следует истинность LS(B1(x: z’1)) Þ QB1(x, z’1). Как следствие, истинно QB1(x, z’1). Из истинности правой части RS3 следует истинность формулы "z1 (QB1(x, z1) Þ PB2(z1)). Как следствие, истинно PB2(z’1). По правилу E2 истинна формула $z2 LS(B2)(z’1, z2). Пусть формула истинна для z’2. Из истинности QB2(z1, z2) Þ PB3(z2) следует истинность PB3(z’2). Аналогичным образом, по индукции доказывается истинность LS(Bj(zj-1: zj)) для j = 1,…, n - 1. Это доказывает реализуемость LS(B1; B2; …, Bn)(x, y).
Допустим, истинна правая часть (5.4). Докажем истинность постусловия Q(x, y). Пусть правая часть (5.4) истинна для z’1, z’2,..., z’n-1. По правилу E3 истинна формула LS(B1(x: z’1)) Þ QB1(x, z’1) и далее – QB1(x, z’1). Истинность QB1(x, z’1) и "z (QB1(x, z) Þ PB2(z)) влечет истинность PB2(z’1). По правилу E3 истинно LS(B2(z’1: z’2)) Þ QB2(z’1, z’2). Поскольку LS(B2(z’1: z’2)) истинно, то истинно QB2(z’1, z’2). Аналогичным образом по индукции доказывается истинность QBj(z’j-1, z’j) для j = 2, …, n - 1. Таким образом, истинна правая часть правила RS4, а значит, и левая, т. е. истинно постусловие Q(x, y). □
Рассмотрим параллельный оператор общего вида со спецификацией в виде предусловия P(x) и постусловия Q(x, y):
P(x) {B1(x: y1) || B2(x: y2) ||...|| Bj(x: yj) ||...|| Bn(x: yn)} Q(x, y) . (5.7)
Здесь x, y1, y2, …, yn - различные непересекающиеся наборы переменных; набор y объединяет в себе наборы y1, y2, …, yn; B1, B2, …, Bn обозначают предикаты и блоки языка P1 со спецификациями (предусловиями и постусловиями) PB1(x), QB1(x, y1), PB2(x), QB2(x, y2), …, PBn(x), QBn(x, yn). Логическая семантика параллельного оператора общего вида определяется на основе логической семантики для двух операторов (см. разд. 4.6):
LS(B1(x: y1) || B2(x: y2) ||...|| Bj(x: yj) ||...|| Bn(x: yn)) º
LS(B1(x: y1)) & LS(B2(x: y2)) & ... & LS(Bj(x: yj)) & ... & LS(Bn(x: yn)) . (5.8)
Допустим, определение предиката A исполняется в рамках секции s. Секция s состоит из переменных наборов x, y1, y2, …, yn. Исполнение оператора (5.7) реализуется на метаязыке оператором runStat(s, K(x:y)) в (4.14) и определяется следующим образом:
runCallBlock(s, B1(x: y1)) || (5.9)
runCallBlock(s, B2(x: y2)) || ... ||
runCallBlock(s, Bj(x: yj)) || ... ||
runCallBlock(s, Bn(x: yn)) .
Определим правила серии L, гарантирующие корректность параллельного оператора общего вида (5.7).
Правило LP4. P(x) ├ PB1(x) & PB2(x) & ... & PBn(x).
Правило LP5. P(x) & Q(x, y) ├ QB1(x, y1) & QB2(x, y2) & ... & QBn(x, yn).
Лемма 5.3. Допустим, спецификация P(x) и Q(x, y) параллельного оператора общего вида реализуема, операторы B1, …, Bn однозначны в области предусловий и корректны, а их спецификации однозначны. Если правила LP4 и LP5 истинны, то параллельный оператор (5.7) является корректным.
Определим правила серии R, гарантирующие корректность параллельного оператора общего вида (5.7).
Правило RP3. P(x) ├ PB1(x) & PB2(x) & ... & PBn(x).
Правило RP4. QB1(x, y1) & QB2(x, y2) & ... & QBn(x, yn) ├ 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: z1); B2(x, z1: z2) ;...; Bj(x, zj-1: zj) ;...; Bn(x, zn-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 со спецификациями (предусловиями и постусловиями) PB(x), QB(x, z, t), PC(x, z), QC(x, z, y).
Оператор суперпозиции (5.11) можно определить через оператор суперпозиции (4.16) и параллельный оператор (4.19) языка CCP следующим образом. Введем определения предикатов B1 и C1:
B1(x: x1, z, t1) º PB(x) {B(x: z, t1) || x1 = x} QB(x, z, t1) & x1 = x ;
C1(x1, z, t1: y, t) º PC(x1, z) {C(x1, z: y) || t = t1} QC(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) ├ PB(x) & "x1, z, t1 ((QB(x, z, t1) & x1 = x) Þ PC(x1, z)).
Правило RS2’. P(x) & $x1,z,t1 (QB(x1, z, t1) & x1 = x & QC(x1, z, y) & t = t1) ├
Q(x,t, y).
Эквивалентные преобразования RS1’ и RS2’ дают правила RS5 и RS6, по форме подобные правилам RS1 и RS2 для простейшего оператора суперпозиции (4.16).
Правило RS5. P(x) ├ PB(x) & "z, t (QB(x, z, t) Þ PC(x, z)).
Правило RS6. P(x) & $z (QB(x, z, t) & (QC(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) ├ PB(x).
Правило LS2’. P(x) & Q(x, t, y) & QB(x, z, t1) & x1 = x ├
PC(x1, z) & QC(x1, z, y) & t = t1.
Эквивалентные преобразования LS1’ и LS2’ дают правила LS6 и LS7.
Правило LS6. P(x) ├ PB(x).
Правило LS7. P(x) & Q(x, t, y) & QB(x, z, t1) ├ PC(x, z) & QC(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 имеет спецификацию PA(x) и QA(x, y), а предикат B - PB(z) и QB(z, t). Если предикаты A и B являются корректными, то корректно следующее определение:
E(x, z: y, t) º PA(x) & PB(z) {A(x: y) || B(z: t)} QA(x, y) & QB(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) ├ PA(x) & PB(z) & "y,t (QA(x, y) & QB(z, t) Þ PC(y, t)).
Правило RS2’. P(x, z) & $y,t (QA(x, y) & QB(z, t) & QC(y, t, u)) ├ Q(x, z, u).
Допустим, операторы A и B являются однозначными; их спецификации PA(x), QA(x, y), PB(z), QB(z, t) также однозначны. Эквивалентные преобразования RS1’ и RS2’ с учетом однозначности предикатов и спецификаций позволяют устранить переменные y и t, что дает правила RS7 и RS8.
Правило RS7. P(x, z) ├ PA(x) & PB(z) & PC(A(x), B(z)).
Правило RS8. P(x, z) & QC(A(x), B(z), u) ├ Q(x, z, u).
В итоге, справедлива следующая лемма.
Лемма 5.7. Пусть предусловие P(x, z) истинно. Допустим, операторы A, B и C корректны, операторы A и B, а также их спецификации PA(x), QA(x, y), PB(z), QB(z, t) однозначны. Если правила RS7 и RS8 истинны, то оператор (5.15) со спецификацией P(x, z) и Q(x, z, u) является корректным.
Для получения правил серии L применим правила LS1 и LS2 для оператора в правой части (5.16). Получим следующие правила.
Правило LS1’. P(x, z) ├ PA(x) & PB(z).
Правило LS2’. P(x, z) & Q(x, z, u) & QA(x, y) & QB(z, t)├ PC(y, t) & QC(y, t, u).
Предполагая однозначность предикатов A и B, а также их спецификаций, проведем эквивалентные преобразования LS1’ и LS2’, устраняя переменные y и t. Получим следующие правила.
Правило LS8. P(x, z) ├ PA(x) & PB(z).
Правило LS9. P(x, z) & Q(x, z, u)├ PC(A(x), B(z)) & QC(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. Аргументация в пользу типового языка заключается в том, что указание типов переменных существенно повышает понимание программы.
Язык предикатного программирования
Введение
Язык предикатного программирования P (Predicate programming language) является универсальным и может использоваться для разработки широкого класса программ. По меньшей мере, этот класс включает программы, разрабатываемые обычно на языке ФОРТРАН, для задач вычислительной математики. В целях спецификации и реализации программ для реактивных систем язык P расширен средствами для описания процессов, передачи сообщений и порождения процессов, работающих параллельно с процессом-родителем. В меньшей степени язык P пригоден для задач системного программирования, где обычно используются объектно-ориентированные средства, которых нет в ядре языка P.
По сложившейся классификации язык P следует отнести к классу языков функционального программирования. Язык P сочетает функциональный и операторный (предикатный) стили записи алгоритмов и обладает существенно большей выразительностью по сравнению с чисто функциональными языками. В этом смысле язык P ближе к языкам логического программирования. Однако в отличие от логических языков процесс вычисления программы на языке P реализуется не логическим выводом, а явным исполнением, характерным для императивных и функциональных языков.
Функциональный язык удобнее императивного для разработки алгоритма. Однако получение эффективной программы для функциональных языков проблематично даже с применением изощренной оптимизации в процессе трансляции. Поэтому после отладки программы на функциональном языке для достижения требуемой эффективности ее приходится переписывать на императивный язык. Приемущество технологии предикатного программирования в том, что она является сквозной: к предикатной программе применяется набор трансформаций с получением эффективной программы на императивном расширении языка P (см. разд. 6.11), после чего программа может конвертироваться на любой из императивных языков: C, C++, ФОРТРАН и др. Базовыми трансформациями являются:
· склеивание переменных, реализующее замену нескольких переменных одной;
· замена хвостовой рекурсии циклом;
· подстановка определения предиката на место его вызова;
· кодирование структурных объектов низкоуровневыми структурами с использованием массивов и указателей.
С помощью данных трансформаций можно получить программу предельной эффективности, однако трудно это сделать автоматически.
Язык предикатного программирования P впервые представлен в работе [1]. Полное описание языка P дается в препринте [2]. Последующие модификации и расширения языка инициированы использованием языка для описания различных алгоритмов [3–5]. Введены средства спецификации определений предикатов в виде предусловий и постусловий. Имеется опыт использования языка P в качестве языка публикации алгоритмов. Язык P расширен для спецификации и реализации реактивных систем, определяемых в виде совокупности взаимодействующих процессов [5]. Введены средства изображения процессов, операторы приема и посылки сообщений, средства динамического порождения процессов.
Все предыдущие версии языка P по стилю были ближе к языкам Паскаль и Модула-2. Последняя версия языка P, представленная в настоящем описании, по синтаксису, набору операторов и операций и другим особенностям существенно приближена к стилю языков типа C. Как следствие, язык P станет более комфортным для программирующих на языках C, C++, Java, C#. Изменения синтаксиса языка P стали причиной проведения серии серьезных модификаций во всем языке. Определенное влияние на новую версию языка P оказал язык спецификаиций PVS [7]. Введены алгебраические типы. Последовательности заменены списками.
Синтаксис описывается на расширенном языке Бэкусовских нормальных форм (БНФ) со следующими особенностями:
· терминальные символы выделены жирным шрифтом;
· [ фрагмент ] - означает возможное отсутствие в синтаксическом правиле заключенного в квадратные скобки фрагмента; фрагмент определяет последовательность терминальных и нетерминальных символов;
· ( фрагмент )* - определяет повторение фрагмента нуль или более раз; круглые скобки могут быть опущены, если фрагмент состоит из одного символа;
· ( фрагмент )+ - определяет повторение фрагмента один или более раз;
· запись вида [:CLASS:] обозначает символ указанного класса; используются следующие классы символов:
alpha - буквенный символ, принадлежащий латинскому или русскому алфавиту; разрешаются заглавные и строчные буквы;
digit - цифра (0, 1, 2, 3, 4, 5, 6, 7, 8 или 9);
alnum - символ, принадлежащий alpha или digit;
blank - пробел или символ табуляции;
xdigit - шестнадцатеричная цифра (digit - заглавная или строчная буква от A до F);
print - символ, для которого определено начертание (т. е. символ из alnum, blank либо какой-либо другой символ, который можно отобразить).
Предикаты
Программа состоит из набора определений предикатов.
Операторы
БЛОК ::= { ОПЕРАТОР }
ОПЕРАТОР ::= [ОПИСАНИЕ-ПЕРЕМЕННЫХ ;]{ ЗАМКНУТЫЙ-ОПЕРАТОР |
[ОПИСАНИЕ-ПЕРЕМЕННЫХ ;] ПАРАЛЛЕЛЬНЫЙ-ОПЕРАТОР |
[ОПИСАНИЕ-ПЕРЕМЕННЫХ ;] ОПЕРАТОР-СУПЕРПОЗИЦИИ
Описанные переменные считаются локальными в теле предиката. Тип локальной переменной может быть также определен описателем var (см. разд. 6.3.3) в случае, когда тип легко определяется из контекста дальнейшего использования переменной.
ЗАМКНУТЫЙ-ОПЕРАТОР ::=
ОПЕРАТОР-ПРИСВАИВАНИЯ | ВЫЗОВ-ПРЕДИКАТА-ФУНКЦИИ |
ВЫЗОВ-ПРЕДИКАТА-ГИПЕРФУНКЦИИ [ОПЕРАТОР-ОБРАБОТКИ-ВЕТВЕЙ] |
УСЛОВНЫЙ-ОПЕРАТОР | БЛОК [ОПЕРАТОР-ОБРАБОТКИ-ВЕТВЕЙ] |
ОПЕРАТОР-ВЫБОРА | ОПРЕДЕЛЕНИЕ-ЛОКАЛЬНОГО-ПРЕДИКАТА
ОПЕРАТОР-ПРИСВАИВАНИЯ ::= ПЕРЕМЕННАЯ = ВЫРАЖЕНИЕ
В результате исполнения оператора присваивания переменной присваивается значение выражения. Типы выражения и переменной должны быть совместимы (см. разд. 6.7).
УСЛОВНЫЙ-ОПЕРАТОР ::=
ОПЕРАТОР-ЕСЛИ else ЗАМКНУТЫЙ-ОПЕРАТОР [ОПЕРАТОР-ПЕРЕХОДА]
ОПЕРАТОР-ЕСЛИ ::= if ( ВЫРАЖЕНИЕ ) ОПЕРАТОР [ОПЕРАТОР-ПЕРЕХОДА]
В операторе перехода указывается либо метка ветви гиперфункции, либо метка ветви обработчика, следующего за блоком, содержащим данный условный оператор.
if (x > 0) s = 1
else if (x < 0) s = -1
else s = 0
Пример 3. Использование условного оператора
ПАРАЛЛЕЛЬНЫЙ-ОПЕРАТОР ::=
ЗАМКНУТЫЙ-ОПЕРАТОР (|| ЗАМКНУТЫЙ-ОПЕРАТОР)+
Операторы, образующие параллельный оператор, должны иметь непересекающиеся наборы результирующих переменных. Исполнение параллельного оператора слагается из исполнения входящих в него операторов. Операторы выполняются независимо друг от друга; они могут исполняться параллельно.
ОПЕРАТОР-СУПЕРПОЗИЦИИ ::= ОПЕРАТОР (; ОПЕРАТОР)+
В цепочке операторов, составляющих оператор суперпозиции, каждый следующий оператор использует значения локальных переменных, присвоенных предыдущими операторами. Каждая пара соседних операторов в цепочке должна быть связана хотя бы одной локальной переменной; если такой связи нет, их композиция должна быть оформлена параллельным оператором.
ЗАГОЛОВОК-ОПЕРАТОРА-ВЫБОРА ::= switch ( ВЫРАЖЕНИЕ )
ОПЕРАТОР-ВЫБОРА ::= ЗАГОЛОВОК-ОПЕРАТОРА-ВЫБОРА
{ ОПЕРАТОР-АЛЬТЕРНАТИВЫ+
[default : ОПЕРАТОР [ОПЕРАТОР-ПЕРЕХОДА]]
}
ОПЕРАТОР-АЛЬТЕРНАТИВЫ ::=
case АЛЬТЕРНАТИВА (, АЛЬТЕРНАТИВА)* : ОПЕРАТОР [
ОПЕРАТОР-ПЕРЕХОДА]
АЛЬТЕРНАТИВА ::= ВЫРАЖЕНИЕ | ОПРЕДЕЛЕНИЕ-КОНСТРУКТОРА
Выполняется тот оператор альтернативы, для которого значение АЛЬТЕРНАТИВЫ совпадает со значением выражения в заголовке оператора выбора. Оператор после default выполняется в случае, когда нет ОПЕРАТОРА-АЛЬТЕРНАТИВЫ с требуемым значением
АЛЬТЕРНАТИВЫ. Трактовка операторов перехода та же, что и для условного оператора.
Если в позиции выражения в заголовке оператора выбора находится переменная типа объединения, то в качестве АЛЬТЕРНАТИВЫ указывается ОПРЕДЕЛЕНИЕ-КОНСТРУКТОРА. Особенности выполнения ОПЕРАТОРА-АЛЬТЕРНАТИВЫ определены в разд. 6.7.
ОПЕРАТОР-ОБРАБОТКИ-ВЕТВЕЙ ::=
(case [МЕТКА-ВЕТВИ-ОБРАБОТЧИКА :] ОПЕРАТОР)+
МЕТКА-ВЕТВИ-ОБРАБОТЧИКА ::= МЕТКА
Оператор обработки ветвей следует за вызовом гиперфункции либо за блоком, содержащем операторы перехода. Если предыдущий оператор нормально завершается, то оператор обработки ветвей игнорируется. Нормальное завершение возможно и для вызова гиперфункции, когда на одной из ветвей гиперфункции опущена метка перехода, что означает суперпозицию (или параллельную композицию) с последующим оператором, а на другой ветви имеется переход на метку ветви обработчика или на метку ветви гиперфункции, в теле которой находится данный оператор.
Исполнение оператора обработки ветвей инициируется оператором перехода, находящимся в предыдущем операторе. При этом исполняется оператор, помеченный соответствующей меткой, после чего исполнение оператора обработки ветвей и предыдущего оператора считается завершившимся.
В вызове гиперфункции могут быть опущены переходы, а в последующем операторе обработки ветвей - метки ветвей обработчика. В этом случае порядок ветвей обработчика соответствует порядку ветвей вызова гиперфункции.
A(i: y #1: #2)
case 1: B(y, i: u)
case 2: D(i: u);
Пример 4.Вызов гиперфункции с обработчиком ветвей
ОПРЕДЕЛЕНИЕ-ЛОКАЛЬНОГО-ПРЕДИКАТА ::= ОПРЕДЕЛЕНИЕ-ПРЕДИКАТА
Определение локального предиката допускает использование параметров и локальных переменных предиката, в теле которого это определение находится. Локальный предикат доступен лишь в теле предиката, внутри которого он описан.
Типы
Всякая переменная имеет некоторый тип. Тип может быть атрибутом языковой конструкции. Семантика конструкции налагает определенные ограничения на значения типов. Для каждой подконструкции некоторой конструкции определяется позиция ее вхождения внутри конструкции. Это, например, позиции операндов операций, позиции правой и левой частей в операторе присваивания, позиция фактического параметра в вызове предиката и др. При наличии в конструкции двух позиций типы этих позиций должны быть согласованы. Частным случаем согласованности является совместимость типов. Например, тип выражения правой части оператора присваивания должен быть совместим с типом переменной левой части оператора присваивания, но не наоборот. Реализуется неявное преобразование (называемое приведением) значения совместимого типа к типу, требуемому позицией.
ОПИСАНИЕ-ТИПА ::=
type ИМЯ-ТИПА [( ПАРАМЕТРЫ-ТИПА )] = ИЗОБРАЖЕНИЕ-ТИПА |
ПРЕДОПИСАНИЕ-ТИПА
ИМЯ-ТИПА ::= ИДЕНТИФИКАТОР
ПАРАМЕТРЫ-ТИПА ::=
ИЗОБРАЖЕНИЕ-ТИПА [:blank:] ИДЕНТИФИКАТОР (, ИДЕНТИФИКАТОР)*
[, ПАРАМЕТРЫ-ТИПА]
Описание типа связывает имя типа с его изображением. Тип может быть параметризован, т. е. зависеть от набора значений переменных и типов, указанных в качестве параметров.
ПРЕДОПИСАНИЕ-ТИПА ::= type ИМЯ-ТИПА
Если имя типа используется до его описания, что возможно для рекурсивных определений типов, то перед первым вхождением имени оно должно быть декларировано с помощью предописания.
ИЗОБРАЖЕНИЕ-ТИПА ::=
ИЗОБРАЖЕНИЕ-ПРИМИТИВНОГО-ТИПА | ИЗОБРАЖЕНИЕ-ТИПА-ПО-ИМЕНИ |
ИЗОБРАЖЕНИЕ-ТИПА-КАК-ПАРАМЕТРА | ИЗОБРАЖЕНИЕ-ТИПА-ПРЕДИКАТА |
ИЗОБРАЖЕНИЕ-ПОДТИПА | ИЗОБРАЖЕНИЕ-ПЕРЕЧИСЛЕНИЯ |
ИЗОБРАЖЕНИЕ-СТРУКТУРНОГО-ТИПА |
ИЗОБРАЖЕНИЕ-ТИПА-ОБЪЕДИНЕНИЯ
ИЗОБРАЖЕНИЕ-ПРИМИТИВНОГО-ТИПА ::=
nat [(РАЗРЯДНОСТЬ-ЦЕЛЫХ)] |
int [(РАЗРЯДНОСТЬ-ЦЕЛЫХ)] |
real [(РАЗРЯДНОСТЬ-ВЕЩЕСТВЕННЫХ)] |
bool | char
Тип nat является подмножеством неотрицательных чисел типа int, char - множество символов некоторого алфавита. Конкретные представления примитивных типов даются в императивном расширении языка (см. разд. 6.11).
Разрядность определяет максимальное число битов в представлении значений типа. Указание разрядности в изображении примитивного типа является частью императивного расширения языка.
Значения типа natсовместимы с типом int, а int - с типом real. Значения типа меньшей размерности совместимы с аналогичными типами большей размерности.
ИЗОБРАЖЕНИЕ-ТИПА-ПО-ИМЕНИ ::= [ИМЯ-МОДУЛЯ .] ИМЯ-ТИПА [( АРГУМЕНТЫ )]
Ранее определенный тип может быть представлен своим именем. Изображение параметризованного типа представляется с конкретными параметрами.
ИЗОБРАЖЕНИЕ-ТИПА-КАК-ПАРАМЕТРА ::= type ИМЯ-ТИПА
Объявление типа в качестве параметра описания типа или определения предиката реализуется описателем type. В качестве обозначения типа может использоваться выражение типа type, которым, например, может являться параметр предиката или параметризованного типа. Например:
type Point (type T) = struct (T x, y);
type Polyline (type T) = list (Point (T));
decimate (type T, list (T) data : list (T) data') {
data' = (data = nil) ?
nil :
data.car + (len(data) < 3 ? nil : decimate(T, data.cdr.cdr))
};
reverse (type T, list (T) data : list (T) data') {
data' = (data = nil) ? nil : reverse (T, data.cdr) + data.car
};
Polyline (real) line = [[ (0.0, 0.0), (0.1, 0.2), (0.2, 0.5),
(0.3, 0.6), (0.4, 0.3), (0.5, 0.0) ]];
Polyline (real) line1 = reverse (decimate (real, line));
// [[ (0.4, 0.3), (0.2, 0.5), (0.0, 0.0) ]]
Пример 7. Использование типов в качестве параметров
В примере выше идентификатор T использован в качестве типа-параметра, а тип real - как фактический параметр.
squareVec (type T, list (T) data : list (T) data') {
data' = (data = nil) ? nil : data.car ^ 2 + squareVec (T, data.cdr)
};
list (int) squares = squareVec (int, [[ 0, 1, 2, 3, 4 ]] ); // [[ 0, 1, 4, 9, 16 ]]
Выше приведен еще один пример использования типа T в качестве параметра предиката.
ИЗОБРАЖЕНИЕ-ТИПА-ПРЕДИКАТА ::=
predicate ОПИСАНИЕ-СПЕЦИФИКАЦИИ-ПРЕДИКАТА
Имя параметра предиката может быть опущено. В этом случае описывается только тип параметра. Изображение типа предиката используется для описания переменной предикатного типа.
type int_list = list (int);
map_list (int_list src, predicate (int : int) func : int_list dest) {
dest = (src = nil) ? nil : func (src.car) + map_list (src.cdr, func))
};
int_list numbers = [[ 0, 1, 2, 3, 4, 5 ]];
int_list squares = map_list (numbers, predicate (int a : int b) { b = a * a; });
// squares = [[ 0, 1, 4, 9, 16, 25 ]]
Пример 8. Использование предикатного типа
ОПРЕДЕЛЕНИЕ-ПОДТИПА ::=
subtype ( ОПИСАНИЕ-ПЕРЕМЕННОЙ : ВЫРАЖЕНИЕ ) |
ИЗОБРАЖЕНИЕ-ДИАПАЗОНА
Конструкция subtype(T x: выражение) определяет подмножество типа T. Описание переменной x действует в пределах этой конструкции. Множество значений переменной x, для которых логическое выражение имеет значение “истина”, является определяемым подтипом типа T. Если выражение содержит другие переменные, то все они являются параметрами изображаемого типа. Конструкция ОПИСАНИЕ-ПЕРЕМЕННОЙ определена в разд. 6.3.3
ИЗОБРАЖЕНИЕ-ДИАПАЗОНА ::= ВЫРАЖЕНИЕ .. ВЫРАЖЕНИЕ
Изображение диапазона является подмножеством типа int, enum или char. Изображение типа subtype(nat i: i >= 1 & i <= n + 1) эквивалентно изображению диапазона: 1 .. n + 1.
type odd_t = subtype (int n: n % 2 = 1);
type diap10_20_t = 10..20;
ИЗОБРАЖЕНИЕ-СТРУКТУРНОГО-ТИПА ::=
ИЗОБРАЖЕНИЕ-ТИПА-СТРУКТУРЫ | ИЗОБРАЖЕНИЕ-ТИПА-ОБЪЕДИНЕНИЯ |
ИЗОБРАЖЕНИЕ-ТИПА- СПИСКА | ИЗОБРАЖЕНИЕ-ТИПА-МНОЖЕСТВА |
ИЗОБРАЖЕНИЕ-ТИПА-МАССИВА
ИЗОБРАЖЕНИЕ-ТИПА-СТРУКТУРЫ ::= struct ( ОПИСАНИЕ-ПОЛЕЙ )
ОПИСАНИЕ-ПОЛЕЙ ::= ИЗОБРАЖЕНИЕ-ТИПА [:blank:] СПИСОК-ИМЕН-ПОЛЕЙ
[, ОПИСАНИЕ-ПОЛЕЙ]
СПИСОК-ИМЕН-ПОЛЕЙ ::= ИМЯ-ПОЛЯ [, СПИСОК-ИМЕН-ПОЛЕЙ]
Значение типа структуры состоит из совокупности значений полей структуры. Имена полей должны быть различны. Число полей должно быть не менее двух.
type Point = struct ( int x, y );
Point pt = (10, 20);
Пример 9. Определение структуры
ИЗОБРАЖЕНИЕ-ТИПА-ОБЪЕДИНЕНИЯ ::= union ( ОПИСАНИЯ-КОНСТРУКТОРОВ )
ОПИСАНИЯ-КОНСТРУКТОРОВ ::=
ОПИСАНИЕ-КОНСТРУКТОРА (, ОПИСАНИЕ-КОНСТРУКТОРА)*
Значением типа объединения является значение одного из конструкторов, перечисленных в списке описаний конструкторов. Число конструкторов должно быть не меньше двух.
ОПИСАНИЕ-КОНСТРУКТОРА ::= ИМЯ-КОНСТРУКТОРА [ ( ОПИСАНИЕ-ПОЛЕЙ ) ]
ИМЯ-КОНСТРУКТОРА ::= ИДЕНТИФИКАТОР
Поля, определяемые в круглых скобках, являются полями объединения. Значения этих полей используются в качестве аргументов конструктора. Имена полей объединения по всем конструкторам должны быть различны.
Работа с объектами типа объединения реализуется с помощью следующих конструкций: конструктор, распознаватель и поле объединения. Все они являются ПЕРВИЧНЫМИ-ВЫРАЖЕНИЯМИ (см. разд. 6.6).
КОНСТРУКТОР ::= ИМЯ-КОНСТРУКТОРА [ ( СПИСОК-ВЫРАЖЕНИЙ ) ]
Выражения, подставляемые в качестве аргументов КОНСТРУКТОРА, по их числу и типам должны соответствовать ОПИСАНИЯМ-ПОЛЕЙ в соответствующем ОПИСАНИИ-КОНСТРУКТОРА. Правила соответствия такие же, как для вызова предиката. Значением конструкции КОНСТРУКТОР является имя конструктора вместе со значениями его аргументов, если аргументы присутствуют.
РАСПОЗНАВАТЕЛЬ ::= ИМЯ-РАСПОЗНАВАТЕЛЯ ( ВЫРАЖЕНИЕ )
ИМЯ-РАСПОЗНАВАТЕЛЯ ::= ИМЯ-КОНСТРУКТОРА ?
Символ “?” является частью имени распознавателя и пишется слитно с именем конструктора, без пробела. ВЫРАЖЕНИЕ имеет тип объединения. Распознаватель является функцией типа bool. Значение РАСПОЗНАВАТЕЛЯ истинно, если значением ВЫРАЖЕНИЯ является конструктор с именем ИМЯ-КОНСТРУКТОРА.
ПОЛЕ-ОБЪЕДИНЕНИЯ ::= ПЕРВИЧНОЕ-ВЫРАЖЕНИЕ . ИМЯ-ПОЛЯ
Значением ПЕРВИЧНОГО-ВЫРАЖЕНИЯ является переменная типа «объединение». Значением ПОЛЯ-ОБЪЕДИНЕНИЯ является значение поля с именем ИМЯ-ПОЛЯ в структуре переменной типа «объединение». Использование конструкции ПОЛЕ-ОБЪЕДИНЕНИЯ корректно лишь в случае истинности распознавателя ИМЯ-КОНСТРУКТОРА?( ПЕРВИЧНОЕ-ВЫРАЖЕНИЕ ) для конструктора, к которому относится поле с именем ИМЯ-ПОЛЯ, в противном случае исполнение конструкции не определено.
Имена конструкторов и распознавателей являются глобально определенными в теле модуля, содержащего ИЗОБРАЖЕНИЕ-ТИПА-ОБЪЕДИНЕНИЯ.
ОПРЕДЕЛЕНИЕ-КОНСТРУКТОРА ::=
ИМЯ-КОНСТРУКТОРА [ ( ОПРЕДЕЛЕНИЕ-ПОЛЕЙ-КОНСТРУКТОРА ) ]
ОПРЕДЕЛЕНИЕ-ПОЛЕЙ-КОНСТРУКТОРА ::=
ОПРЕДЕЛЕНИЕ-ПОЛЯ-КОНСТРУКТОРА
[, ОПРЕДЕЛЕНИЕ-ПОЛЕЙ-КОНСТРУКТОРА]
ОПРЕДЕЛЕНИЕ-ПОЛЯ-КОНСТРУКТОРА ::=
[ИЗОБРАЖЕНИЕ-ТИПА-ПЕРЕМЕННОЙ] ИДЕНТИФИКАТОР
Конструкция ОПРЕДЕЛЕНИЕ-КОНСТРУКТОРА используется в качестве
АЛЬТЕРНАТИВЫ после case в операторе выбора (см. разд. 6.5) для выражения типа объединения. Значением АЛЬТЕРНАТИВЫ является конструктор с именем ИМЯ-КОНСТРУКТОРА и набором переменных, обозначающих поля данного конструктора. Эти переменные являются локальными в ОПЕРАТОРЕ-АЛЬТЕРНАТИВЫ, исполняемом для данной АЛЬТЕРНАТИВЫ. Типы переменных могут не указываться, поскольку они определяются из ИЗОБРАЖЕНИЯ-ТИПА-ОБЪЕДИНЕНИЯ.
type int_tree = union (
leaf (int val),
node (int_tree lhs, int v, int_tree rhs)
);
int_tree foo;
// ...
switch (foo) {
case leaf(v0): print("leaf", v0)
case node(l, v1, r): print("node with ", v1)
};
int_tree one_leaf = leaf(42);
int_tree small_tree = node(leaf(1), 2, node(leaf(3), 4, leaf(5)));
// small_tree задаёт следующее дерево:
// 2
// /
// 1 4
// /
// 3 5
Пример 10. Использование объединений
ИЗОБРАЖЕНИЕ-ПЕРЕЧИСЛЕНИЯ ::=
enum ( ИДЕНТИФИКАТОР (, ИДЕНТИФИКАТОР)* )
Тип перечисления является частным случаем типа объединения с конструкторами без аргументов. Описатель enum трактуется как эквивалент union.
type fruit = enum (apple, orange, banana);
Пример 11. Описание перечисления
Структура вида “список” представляется как упорядоченная совокупность однородных элементов. Тип списка из элементов типа T определяется следующим описанием:
type list (type T) = union (
nil,
cons (T car, list(T) cdr)
);
Тип list считается определенным в языке P и не требует описания в программе. Имена list, nil и cons глобально определены в предикатной прграмме.
Конструктор nil определяет пустой список, не содержащий элементов. Остальные значения типа list представляются конструктором cons(x, s), где элемент x есть первый элемент списка - голова списка, а s есть оставшаяся часть списка - хвост списка. Функция len(s) определяет число элементов списка s. Операция конкатенации s1 + s2 определяет список, состоящий из элементов списка s1, за которыми следуют элементы списка s2. Аргументами конкатенации могут быть также элементы списка. Функция last(s) определяет последний элемент непустого списка s; функция prec(s) - оставшуюся часть списка без последнего элемента.
ЭЛЕМЕНТ-СПИСКА ::= ПЕРВИЧНОЕ-ВЫРАЖЕНИЕ [ ИНДЕКС-ЭЛЕМЕНТА ]
Данная конструкция определяет значение элемента с указанным индексом в списке. Значением ПЕРВИЧНОГО-ВЫРАЖЕНИЯ является список.
ИНДЕКС-ЭЛЕМЕНТА ::= ВЫРАЖЕНИЕ
Для списка s конструкция s[i] определяет i-й элемент. Допустимыми являются значения индекса i от 0 до len(s) - 1.
type int_list = list (int);
int_list s = [[ 1, 1, 2, 3, 5, 8 ]];
int s_car = s.car; // s_car = 1
int_list s_cdr = s.cdr; // s_cdr = [[ 1, 2, 3, 5, 8 ]]
int_list ss = s + [[ 13, 21 ]]; // ss = [[ 1, 1, 2, 3, 5, 8, 13, 21 ]]
int count = len (s); // count = 6
int e = s[3]; // e = 3
Пример 12. Операции со списком
СТРОКОВЫЙ-ТИП ::= string
Строковый тип string является обозначением типа списка list(char). В дополнение к определенным выше операциям со списками имеется возможность задания конкретного значения строкового типа в виде строковой константы (см. разд. 6.2).
ИЗОБРАЖЕНИЕ-ТИПА-МНОЖЕСТВА ::= set ( ИЗОБРАЖЕНИЕ-БАЗОВОГО-ТИПА )
ИЗОБРАЖЕНИЕ-БАЗОВОГО-ТИПА ::= ИЗОБРАЖЕНИЕ-ТИПА
Тип множества есть множество всех подмножеств некоторого конечного базового типа. Имеется унарная операция ~ дополнения множества. Определены: операция «+» сложения множеств, операция «-» вычитания множеств, а также вычитания элемента из множества, операция & пересечения множеств, операция or объединения множеств, операция in принадлежности элемента множеству (см. разд. 6.6). Число элементов в множестве реализуется функцией len.
Операция mask преобразует множество в целое значение. Операция bits реализует обратную операцию преобразования целого в множество.
type int_set_t = set (1..1000);
int_set_t pow_2 = { 0, 2, 4, 8, 16, 32 };
bool is_pow_2 = 4 in pow_2; // is_pow_2 = true
int_set_t more_pow_2 = pow_2 + { 64, 128 };
Пример 13. Использование множеств
Массивы
Список литературы
1. Шелехов В. И. Введение в предикатное программирование. Новосибирск, 2002. 82 с. (Препр. / ИСИ СО РАН № 100).
2. Шелехов В. И. Язык предикатного программирования P. Новосибирск, 2002. 40 с. (Препр. / ИСИ СО РАН № 101).
3. Шелехов В. И. Предикатное программирование: основы, язык, технология // Методы предикатного программирования. Новосибирск, ИСИ СО РАН. 2003. С. 7-15.
4. Шелехов В. И. Разработка программы построения дерева суффиксов в технологии предикатного программирования. Новосибирск, 2004. 52 с. (Препр. / ИСИ СО РАН № 115).
5. Шелехов В. И. Язык спецификации процессов // Методы предикатного программирования. Новосибирск, ИСИ СО РАН. 2006. Вып. 2. C. 17-34.
6. Шелехов В. И. Модель корректности программ на языке исчисления вычислимых предикатов. Новосибирск, 2007. 51 с. (Препр. / ИСИ СО РАН № 145).
7. PVS Specification and Verification System. URL: http://pvs.csl.sri.com/
8. Milner R. A Calculus of Communicating Systems // LNCS. Springer Verlag, 1980. Vol. 94.
9. Lamport L. Specifying concurrent systems with TLA+. Calculational System Design. Series F: Computer and Systems Sciences. Amsterdam: IOS Press. 1999. N. 173. P. 183-247.
10. Moura L., Owre S., and Shankar N. The SAL Language Manual. SRI International. URL: http://sal.csl.sri.com/doc/language-report.pdf.
Пример. Сортировка простыми вставками
Рассмотрим задачу сортировки простыми вставками [6]. На ее примере демонстрируются типовые методы построения предикатных программ, доказательства их корректности и получения эффективных программ. Представлен нетривиальный способ кодирования списков.
В алгоритме [6] сортируемый список s рассматривается в виде конкатенации u + b + v, где u и v - списки, а b - элемент, причем список u - сортированный.
На очередном шаге работы алгоритма элемент b вставляется внутрь списка u таким образом, чтобы сохранить сортированность обновленного списка u. На следующем шаге в качестве элемента b рассматривается начальный элемент v, и процесс повторяется.
Элементы списка имеют произвольный тип T с линейным порядком “£”. Типы элементов и списков представлены описаниями:
type T{ £ : axiom "a. a £ a, axiom "a, b. a £ b & b £ a Þ a = b,
axiom "a, b, c. a £ b & b £ c Þ a <= c, axiom "a, b. a £ b Ú b £ a };
type S = list (T);
Свойство сортированности списка s определяется предикатом:
SORT(s) @ "s1, s2 Î S. "a, b Î T. (s = s1 + a + b + s2 Þ a £ b)
Лемма 7.1. Список не более, чем из одного элемента - сортированный, т. е. SORT(nil) & "a. SORT([[a]]).
Лемма 7.2. length(s) ≤ 1 Û s = nil Ú $a. s = [[a]].
Лемма 7.3. length(s) ≤ 1 Þ SORT(s).
Допустим, список v является результатом сортировки исходного списка u. Списки u и v состоят из одной и той же совокупности элементов. Тогда список v можно получить из u применением серии перестановок элементов. Обозначим это свойство через PERM(u, v). Элементарную перестановку можно определить предикатом:
perm(u, v) @ $s1,s2,s3ÎS. $a,bÎT. u = s1 + a + s2+ b + s3 & v = s1 + b + s2+ a + s3
Тогда свойство перестановочности PERM(u, v) можно определить следующим образом:
PERM(u, v) @ u = v Ú $ w. perm(u, w) & PERM(w, v) .
Приведенное рекурсивное определение эквивалентно следующему нерекурсивному:
PERM(u, v) º $n³1. $w1…wn Î S. u = w1 & v = wn & "i=1..n-1. perm(wi, wi+1) .
Лемма 7.4. length(u) ≤ 1 & PERM(u, v) Þ u = v.
Доказательство. Пусть истинны length(u) ≤ 1 и PERM(u, v). Предикат perm(u, w) - ложный для любого списка w, поскольку в определении предиката u должна содержать не менее двух элементов. Поэтому ложна вторая альтернатива предиката PERM(u, v), а значит, истинна первая, т. е. u = v. □
Спецификацию задачи сортировки представим определением:
sort(S s: S s’) post SORT(s’) & PERM(s, s’);
Напомним, что штрих в имени s’ предполагает склеивание переменных s и s’ в реализации, см. разд. 6.3.
Сначала задачу sort следует свести к более общей задаче sort1, в которой s = u + b + v, где u и v - списки, а b - элемент, причем список u - сортированный. Спецификация задачи sort1 следующая:
sort1(S u, T b, S v: S r) pre u ≠ nil & SORT(u) post SORT(r) & PERM(u + b + v, r);
Лемма 7.5. Спецификация sort1 реализуема и однозначна, т. е. существует единственный список r, удовлетворяющий постусловию.
Возможность сведения задачи sort к sort1 обеспечивается следующей леммой.
Лемма 7.6. length(s) > 1 Þ s = s.car + s.cdr.car + s.cdr.cdr.
Дадим определение предиката sort и докажем его корректность.
sort(S s: S s’)
{ if (length(s) ≤ 1) s' = s
else sort1(s.car, s.cdr.car, s.cdr.cdr: s')
} post SORT(s’) & PERM(s, s’);
Доказательство корректности. Поскольку спецификация реализуема, а тело предиката sort - однозначный оператор, то в соответствии с теоремой 2.1 тождества спецификации и программы достаточно доказать истинность тела предиката из постусловия. Пусть SORT(s’) и PERM(s, s’) истинны. Пусть истинно условие length(s) ≤ 1. Истинность оператора s' = s следует из леммы 7.4. Пусть истинно условие length(s) > 1. Докажем истинность вызова sort1. Прежде всего, истинны условия корректности для полей car и cdr, поскольку s и s.cdr отличны от nil. Далее, истинно предусловие для аргументов вызова sort1, т. е. истинны SORT(s.car) (по лемме 7.3) и s.car ¹ nil. По лемме 2.8. предикат sort1 тождественен постусловию. Поэтому достаточно доказать истинность формулы:
SORT(s’) & PERM(s.car + s.cdr.car + s.cdr.cdr, s’).
Ее истинность следует из леммы 7.6 и предусловия sort. □
Задача sort1 содержит независимую подзадачу pop_into вставки элемента b внутрь отсортированного списка u:
pop_into(S u, T b: S w) pre u ≠ nil & SORT(u) post SORT(w) & PERM(u + b, w);
Лемма 7.7. Спецификация pop_into реализуема и однозначна.
Дадим определение предиката sort1 и докажем его корректность.
sort1(S u, T b, S v: S r) pre u ≠ nil & SORT(u)
{ pop_into(u, b:S w);
if (v = nil ) r = w
else sort1(w, v.car, v.cdr: r)
} post SORT(r) & PERM(u + b + v, r);
Доказательство. Доказательство истинности тела предиката из предусловия и постусловия сводится к доказательству истинности условного оператора. Предусловие оператора pop_into(u, b:S w) истинно. Поэтому оператор полагается истинным при доказательстве истинности условного оператора. Мы можем заменить его постусловием SORT(w) & PERM(u + b, w). Переменная v является индуктивной. Используется отношение порядка: v ⊑ t @ $q. q + v = t. Тогда истинно v.cdr ⊏ v. Минимальный элемент nil покрывается условием v = nil в условном операторе. Пусть истинно условие v = nil. Тогда из истинности PERM(u + b, r) и PERM(u + b, w) следует истинность оператора r = w. Ввиду истинности предусловия операций v.car и v.cdr, истинности предусловия рекурсивного вызова sort1 и истинности v.cdr ⊏ v в соответствии с индуктивным предположением можно заменить вызов sort1 постусловием SORT(r) & PERM(w + v, r). Истинность PERM(w + v, r) следует из истинности PERM(u + b, w) и PERM(u + b + v, r). □
Задачу pop_into необходимо свести к более общей задаче pop_into1, в которой u = y + a + z, где текущий элемент a разделяет списки y и z; при этом все элементы из z больше, чем b. Спецификация задачи pop_into1 следующая:
pop_into1(S y, z, T a, b: S w) pre SORT(y + a + z) & (z ≠ nil Þ b ≤ z.car)
post SORT(w) & PERM(y + a + b + z, w);
Лемма 7.8. Спецификация pop_into1 реализуема и однозначна.
Дадим определение предиката pop_into и докажем его корректность.
pop_into(S u, T b: S w) pre u ≠ nil & SORT(u)
{ pop_into1(prec(u), nil, last(u), b: w)
} post SORT(w) & PERM(u + b, w);
Доказательство. Нетрудно проверить истинность предусловия вызова pop_into1. Заменим вызов pop_into1 его постусловием SORT(w) & PERM(u + b, w) и обнаружим, что оно совпадает с постусловием pop_into, что доказывает его истинность. □
Определение pop_into1 реализуется разбором случаев. Докажем его корректность.
pop_into1(S y, z, T a, b: S w) pre SORT(y + a + z) & (z ≠ nil Þ b ≤ z.car)
{ if (a ≤ b) w = y + a + b + z
else if (y = nil) w = b + a + z
else pop_into1(prec(y), a + z, last(y), b: w)
} post SORT(w) & PERM(y + a + b + z, w);
Доказательство. Из предусловия и постусловия докажем истинность объемлющего условного оператора. Пусть истинно условие a ≤ b. Тогда список y + a + b + z является сортированным. Истинность оператора w = y + a + b + z следует из леммы 7.9.
Лемма 7.9. PERM(v, w) & SORT(v) & SORT(w) Þ v =w.
Пусть истинно a > b. Доказательство истинности внутреннего условного оператора проводится индукцией по переменной y. Отношение порядка несколько иное по сравнению с используемым в предикате sort1: y ⊑ t @ $q. y + q = t. Минимальный элемент nil покрывается условием y = nil в условном операторе. Пусть истинно y = nil. Тогда список b + a + z является сортированным и по лемме 7.9 истинен оператор w = b + a + z. Ввиду истинности предусловия операций prec(y) и last(y), истинности предусловия рекурсивного вызова pop_into1 и истинности prec(y) ⊏ y в соответствии с индуктивным предположением можно заменить вызов pop_into1 его постусловием SORT(w) & PERM(y + b + a + z, w). Истинность PERM(y + b + a + z, w) следует из истинности PERM(y + b + a + z, y + a + b + z). □
Применим к предикатной программе сортировки, составленной из определений предикатов sort, sort1, pop_into и pop_into1, систему трансформаций для получения эффективной императивной программы. На первом этапе реализуются склеивания переменных. Ниже приводится результат склеивания для первых трех предикатов; в pop_into1 склеиваний не производится. Перед определением предиката перечисляется список применяемых склеиваний. Отметим, что замена s ¬ r не является склеиванием - она делается для облегчения проведения дальнейшей подстановки определения.
s ¬ s’
sort(S s: S s)
{ if (length(s) ≤ 1) s = s
else sort1(s.car, s.cdr.car, s.cdr.cdr: s)
}
s ¬ r; u ¬ w;
sort1(S u, T b, S v: S s)
{ pop_into(u, b: S u);
if (v = nil ) s = u
else sort1(u, v.car, v.cdr: s)
}
u ¬ w;
pop_into(S u, T b: S u)
{ pop_into1(prec(u), nil, last(u), b: u) };
На втором этапе трансформаций заменим хвостовую рекурсию циклом в определениях sort1 и pop_into1. Раскроем групповые операторы присваивания и оформим циклы. При раскрытии группового оператора в pop_into1 возникает две коллизии, которые устраняются перестановками присваиваний.
sort1(S u, T b, S v: S s)
{ for (; ;) {
pop_into(u, b: S u);
if (v = nil ) {s = u; break}
else { b = v.car; v = v.cdr}
}
}
pop_into1(S y, z, T a, b: S u)
{ for (; ;) {
if (a ≤ b) { u = y + a + b + z; break}
else if (y = nil) { u = b + a + z; break}
else {z = a + z; a = last(y); y = prec(y)}
}
}
На третьем этапе подставим sort1 на место вызова в sort и pop_into1 в pop_into.
sort(S s: S s)
{ if (length(s) ≤ 1) return
S u =s.car; T b = s.cdr.car; S v = s.cdr.cdr;
for (; ;) {
pop_into(u, b: S u);
if (v = nil ) {s = u; break}
else { b = v.car; v = v.cdr}
}
}
pop_into(S u, T b: S u)
{ T a = last(u); S y = prec(u); S z = nil;
for (; ;) {
if (a ≤ b) { u = y + a + b + z; break}
else if (y = nil) { u = b + a + z; break}
else {z = a + z; a = last(y); y = prec(y)}
}
}
Далее, подставим определение pop_into на место вызова в sort.
sort(S s: S s)
{ if (length(s) ≤ 1) return ;
S u = s.car; T b = s.cdr.car; S v = s.cdr.cdr;
for (; ;) {
T a = last(u); S y = prec(u); S z = nil;
for (; ;) {
if (a ≤ b) { u = y + a + b + z; break}
else if (y = nil) { u = b + a + z; break}
else {z = a + z; a = last(y); y = prec(y)}
}
if (v = nil ) {s = u; break}
else { b = v.car; v = v.cdr}
}
}
На четвертом этапе реализуется кодирование списков s, u, v, y и z вырезками одного массива. Особенность кодирования в том, что списки u и v находятся внутри s, а y и z - внутри u. Тип массива представим описанием:
type SEQ(int p, q) = array p..q of T;
Пусть список w кодируется вырезкой W[p..q]. Кодирование используемых в программе конструкций реализуется следующим образом:
S w ® SEQ(p, q)
w = nil → p > q
length(w) → q – p + 1
b = w.car; w := w.cdr → b := W[p]; p := p + 1
a = last(w); w := prec(w) → a := W[q]; q := q – 1
Пусть список s кодируется вырезкой K[0..n].
int n; // номер последнего элемента списка
SEQ(0, n) K;
Пусть s = u + b + v. Здесь u и v являются частью списка s и кодируются вырезками массива K. Пусть позиция элемента b в массиве K есть i. Тогда
u → K[0 .. i - 1]; b → K[ i ]; v → K[i + 1 .. n] . (7.11)
Отметим, что здесь один индекс i используется для представления двух соседних списков u и v. Особенность в том, что изменение индекса i определяет синхронное изменение этих списков. Аналогичным образом реализуется представление для u = y + a + b + z.
В представлении используется другой индекс j.
y → K[0..j - 2]; a → K[j - 1]; b → K[j]; z→ K[j + 1 .. i] .
Позиция элемента b здесь иная, нежели в представлении (7.11). Другая особенность: позиция последнего элемента z совпадает с позицией b в (7.11). Это значит, что весь список z сдвинут на один элемент по сравнению с тем положением, которое имеет z в составе u в (7.11).
Приведем программу, полученную в результате кодирования списков вырезками массива. В ней описание с инициализацией int i = 1 используется как эквивалент двух конструкций S u = s.car и S v = s.cdr.cdr, которым соответствуют вырезки K[0..0] и K[2..n]. Аналогичным образом конструкция int j = i используется вместо S y = prec(u) и S z = nil, отображающихся в вырезки K[0..i - 2] и K[i + 1 .. i]. Кроме того, используется кодирование z = a + z → K[j] = a.
sort(S s: S s)
{ if (n ≤ 0) return ;
int i = 1; T b = K[1];
for (; ;) {
T a = K[i - 1]; int j = i;
for (; ;) {
if (a ≤ b) { K[j] = b; break}
else if (j < 2) { K[0] = b; K[1] = a; break}
else {K[j] = a; a = K[j - 2]; j = j - 1 }
}
if (i >= n) break
else { b = K[i + 1]; i = i + 1 }
}
}
Наконец, приведем итоговую программу сортировки, отличающуюся от предыдущей деталями оформления циклов и упрощением условий.
type SEQ(int p, q) = array p..q of T;
int n; //номер последнего элемента списка
SEQ(0, n) K;
...
if (n ≤ 0) return ;
T b = K[1];
for (int i = 1; ;) {
T a = K[i - 1];
for (int j = i; ; j = j – 1) {
if (a ≤ b) { K[j] = b; break}
else if (j = 1) { K[0] = b; K[1] = a; break }
else { K[j] = a; a = K[j - 2] }
}
if (i = n) break
else { i = i + 1; b = K[i] }
}
Приведенный пример построения программы сортировки простыми вставками в достаточной степени демонстрирует стиль и технологию предикатного программирования. Корректность предикатной программы строго доказывается применением системы правил, определенных в разд. 2 и 5. Эффективность и компактность итоговой программы не хуже написанной вручную. Отметим нетривиальность применяемого синхронного способа кодирования смежных списков с использованием общего индекса.
Можно отметить следующую неэффективность итоговой программы. Если после выполнения оператора b = K[i] обнаруживается, что a ≤ b для a = K[i - 1], то оператор K[j] = b является избыточным. Данный недостаток легко устраняется другим алгоритмом, представленным ниже. Отметим, что предикатное программирование обладает гораздо большей гибкостью в сравнении с императивным и позволяет эффективно реализовать любое проектное решение.
pop_into(S u, T b: S w) pre u ≠ nil & SORT(u)
{ T a = last(u);
if (a ≤ b) w = u + b
else pop_into2(prec(u), a, b: w)
} post SORT(w) & PERM(u + b, w);
pop_into2(S y, z, T b: S w) pre SORT(y + z) & z ≠ nil & b ≤ z.car
{ if (y = nil) w = b + z
elseT c = last(y);
if (c ≤ b) w = y + b + z
else pop_into2(prec(y), c + z, b: w)
} post SORT(w) & PERM(y + b + z, w);
Императивная программа, полученная по этой версии предикатной программы, более эффективна, однако несколько сложнее и длиннее. Данный алгоритм используется в работе [7], однако представлен для массивов, а не списков. Использование массивов вместо списков делает алгоритм существенно сложнее. Намного сложнее становится доказательство корректности, поскольку программа представляется логикой второго порядка.
Else
{ {char b = r.car || string q = r.cdr};
if (цифра(b)) взятьЧисло(q, p * 10 + val(b): v, t)
else {v = p || t = q}
}
} post $w. конецЧисла(r, w, t) & val1(w, p, v);
Доказательство. Пусть истинно постусловие предиката взятьЧисло. Докажем истинность тела предиката. Пусть истинно условие r = nil. Тогда w = nil и t = nil. Далее, v = p. Это доказывает истинность оператора v = p || t = r. Пусть истинно условие r ¹ nil. Докажем истинность второй альтернативы внешнего условного оператора. Истинны условия корректности для полей car и cdr. Далее достаточно доказать истинность внутреннего условного оператора при b = r.car и q = r.cdr. Тогда r = b + q. Пусть истинно условие цифра(b). Докажем истинность рекурсивного вызова. Поскольку q ⊏ r, а для r = nil корректность предиката доказана, то рекурсивный вызов можно заменить его постусловием:
$h. конецЧисла(q, h, t) & val1(h, p * 10 + val(b), v) . (7.37)
Докажем истинность (7.37). Поскольку r = b + q и цифра(b), то w = b + h для некоторого h и истинно конецЧисла(q, h, t). Из определения val1 при r ¹ nil следует, что val1(w, p, v) º val1(h, p * 10 + val(b), v). В итоге, истинна формула (7.37). □
Определения предикатов СуммаСтроки, Сумма, перваяЦифра, числоВстроке и взятьЧисло образуют полную предикатную программу. Рассмотрим процесс ее трансформации для получения эффективной императивной программы. На первом этапе реализуются склеивания переменных. Полный перечень склеиваемых переменных представлен ниже.
Сумма: n ¬ m; s ¬ r, t;
перваяЦифра: s ¬ r, u; e ¬ a;
числоВстроке: s ¬ r, t;
взятьЧисло: ¬ r, q, t; v ¬ p;
Замена склеиваемых переменных на внешнюю переменную s делается в определениях предикатов числоВстроке и взятьЧисло для упрощения последующей подстановки определений на место вызовов. Представим результат склеивания переменных.
СуммаСтроки(string s: nat n){Сумма(s, 0: n)};
Сумма(string s, nat n : nat n)
{ перваяЦифра(s: : char e, string s)
case n = n
case {числоВстроке(e, s: nat v, string s); Сумма(s, n + v:n)}
}
перваяЦифра(string s: : char e, string s)
{ if (s = nil) #1
else {
{ e = s.car || s = s.cdr };
if (цифра(e)) { s = s ||e = e #2}
else перваяЦифра(s: #1 : e, s #2)
}
}
числоВстроке(char e, string s: nat v, string s)
{ взятьЧисло(s, val(e): v, s) }
взятьЧисло(string s, nat v: nat v, string s)
{ if (s = nil) {v = v || s = s}
Else
{ {char b = s.car || s = s.cdr};
if (цифра(b)) взятьЧисло(s, v * 10 + val(b): v, s)
else {v = v || s = s}
}
};
На втором этапе трансформаций заменим хвостовую рекурсию циклом в определениях Сумма, перваяЦифра и взятьЧисло. Удаляются операторы вида n = n. Как следствие, удаляется оператор продолжения case n = n, что требует явного указания переходов от вызова гиперфункции. Раскроем групповые операторы присваивания и оформим циклы.
СуммаСтроки(string s: nat n){Сумма(s, 0: n)};
Сумма(string s, nat n : nat n)
{ for (; ;) {
перваяЦифра(s: #M1 : char e, string s #2)
case 2: {числоВстроке(e, s: nat v, string s); n= n + v}
}
M1:
}
перваяЦифра(string s: #1 : char e, string s #2)
{ for (; ;) {
if (s = nil) #1
else {
{ e = s.car || s = s.cdr };
if (цифра(e)) #2
else {}
}
}
}
числоВстроке(char e, string s: nat v, string s)
{ взятьЧисло(s, val(e): v, s) }
взятьЧисло(string s, nat v: nat v, string s)
{ for (; ;) {
if (s = nil) break
Else
{ {char b = s.car || s = s.cdr};
if (цифра(b)) v = v * 10 + val(b)
Заключение
Технология предикатного программирования предоставляет аппарат для доказательства корректности предикатных программ. При наличии спецификации в виде предусловия и постусловия для каждого определяемого предиката корректность предикатной программы может быть доказана строго математически. Используемая техника доказательства базируется на системе правил доказательства корректности для конструкций языка P. Здесь демонстрировалась техника, соответствующая правилам серии L для однозначных программ и спецификаций. Это техника доказательства в стиле синтеза программы. Логика, применяемая в процессе доказательства, аналогична той, которую обычно использует программист при построении программы. Процесс доказательства хорошо структурирован и даже для большой программы состоит из небольших независимых частей, что предопределяет возможность успешной автоматизации доказательства корректности предикатных программ.
Язык предикатного программирования позволяет писать программы в естественной логике и при этом обладает гораздо большей выразительностью в сравнении с языками императивного программирования. На языке предикатного программирования можно записать любой алгоритм (для задач с предикатной спецификацией), который представим на императивном языке. Аппарат гиперфункций предоставляет новые возможности адекватного и эффективного представления алгоритма. Гиперфункциям нет аналогов в императивных языках. Эффективность в предикатном программировании обеспечивается применением серии оптимизирующих трансформаций. В результате получается императивная программа, которая по эффективности не хуже написанной вручную и почти всегда короче.
Список литература
1. Мир Лиспа. Методы и системы программирования: Пер. с англ. М.: Мир, 1990. Т. 2. 318 с.
2. Ершов А. П. Введение в теоретическое программирование. М.: Наука, 1977. 288 с.
3. Поттосин И. В. Направленные преобразования линейного участка // Языки и системы программирования. Новосибирск, 1981. С. 14-28. (Сб./ВЦ СО АН СССР).
4. Bacon D., Graham S., Sharp O. Compiler transformations for high-performance computing // ACM Computing surveys. 1994. Vol. 26. No. 4. P. 345-420.
5. Петров Э. Ю. Склеивание переменных в предикатной программе // Методы предикатного программирования. Новосибирск, 2003. С. 48-61.
6. Кнут Д. Искусство программирования для ЭВМ. Сортировка и поиск: Пер. с англ. М.: Мир, 1978. Т.3. 843 с.
7. Шелехов В. И., Карнаухов Н. С. Демонстрация технологии предикатного программирования на задаче сортировки простыми вставками // Методы предикатного программирования. Новосибирск, 2003. С. 16-21.
[1] Первые программы писала математик Ада Лавлейс, дочь поэта лорда Байрона, для спроектированной, но не реализованной вычислительной машины Чарльза Беббиджа в 1830-х гг.
[2] Здесь и далее имеется в виду исчисление предикатов высших порядков.
[3] К статической семантике относятся правила идентификации переменных и других объектов программы, совокупность ограничений для значений атрибутов конструкций и система умолчаний.
[4] CCP - Calculus of Computable Predicates.
[5] Практически все языки функционального программирования содержат расширения, включающие конструкции императивного программирования в целях повышения эффективности программ. Такие языки не являются чистыми.
[6] Родственным, но не совпадающим является понятие слабейшего предусловия, введенное Э. Дейкстра [1]; E. Hehner использует термин «точное предусловие» для уточнения [15].
[7] Данная тройка совпадает с (2.5).
[8] Данная тройка совпадает с (2.11).
[9] Эта тройка совпадает с (2.12).
[10] Эта тройка совпадает с (2.13).
[11] Предикат b(t) может оказаться истинным для других элементов t, не являющихся минимальными.
[12] Термов в смысле языка исчисления предикатов
[13] Размеченное объединение в терминологии Т. Хоара [2].
[14] Здесь и далее параметром функции LS является произвольная языковая конструкция. Запись функции LS отличается от используемой в гл. 2.
[15] Если H - переменная предикатного типа, то будем считать, что H входит в набор x.
[16] Чтобы не загромождать пример, используется оператор суперпозиции более общего вида по сравнению с (4.18).
[17] Не обеспечивается даже монотонность для Øb & (x, y) Î Q.
[18] Здесь и далее используется иная форма записи тройки Хоара по сравнению с {P(x)} S {Q(x, y)} в гл. 2.
[19] На самом деле однозначность проверять не требуется, однако для неоднозначной спецификации будет невозможно доказать истинность правил RR3 и RR4.
[20] Ввиду возможной погрешности обычно используют условие det(a) > e с константой e, близкой к нулю.