рефераты конспекты курсовые дипломные лекции шпоры

Реферат Курсовая Конспект

Предикатное программирование

Предикатное программирование - раздел Программирование, Федеральное Агентство По Образованию ...

ФЕДЕРАЛЬНОЕ АГЕНТСТВО ПО ОБРАЗОВАНИЮ

НОВОСИБИРСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

Факультет информационных технологий

 

В. И. ШЕЛЕХОВ

Предикатное программирование

 

Учебное пособие

Новосибирск

УДК 004.432.42 ББК 22.183.492 Ш 427

Оглавление

Введение в курс предикатного программирования .............................................................. 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

Язык исчисления вычислимых предикатов,

4.1. Структура программы на языке CCP ............................................................................ 27 4.2. Система типов данных… 4.3. Логическая и операционная семантика языка CCP .................................................... 31

Семантика языка предикатного программирования.

5.1. Язык P1: подстановка определения предиката на место вызова ............................... 47 5.2. Язык P2: оператор суперпозиции и параллельный оператор общего вида… 5.3. Язык P2: другое обобщение оператора суперпозиции ............................................... 50

Введение .......................................................................................................................... 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. Модель применения программы Описание преобразования информации, реализуемого вычислением программы, называется спецификацией программы.…

Формы спецификации программы

Спецификация называется предикатной, если она эксплицируема в виде формулы на языке исчисления предикатов [2]. Такая экспликация возможна для… Предикатная спецификация есть условие математической задачи, исходными данными… Спецификация называется процессной, если эффект исполнения программы определяется в виде процесса. Процесс исполнения…

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

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.


Корректность программ с предикатной спецификацией

Представление о правильности программы принято формулировать в виде понятия корректности программы. Корректность определяется условиями… Чтобы полностью записать условие корректности, определяющее истинность… Используя логическую семантику, можно построить формулу тотальной корректности программы.

Предикатная спецификация программы

Спецификация P(x) & Q(x, y) является предикатной при условии, что взаимодействие программы с окружением ограничивается вводом данных перед…

Логическая семантика языка программирования

Проанализируем происхождение логики программы. На рис. 2 представлена общая схема, отражающая связи задачи и программы. Программа является… Рис. 2. Связи между задачей и программой

Модель корректности программы

{P(x)} S {Q(x, y)} . (2.5) Здесь программа представлена оператором S, x - набор входных данных, y - набор… Закон соответствия программы и спецификации, сформулированный в разд. 2.1, очевидным образом конкретизируется для…

Система правил доказательства корректности операторов

Понятие корректности, введенное для программы в целом, применимо также к произвольным операторам программы. Допустим, для некоторого оператора 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. □

Система правил вывода программы из спецификации

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

"xÎX "y1,y2. H(x, y1) & H(x, y2) Þ y1 = y2 . Отметим, что однозначный предикат в некоторой области X не обязательно… Оператор S является однозначным в области X, если формула LS(S)(x, y) однозначна в области X. Нетрудно убедиться, что…

Теорема тождества спецификации и программы

Теорема 2.1 тождества спецификации и программы. Рассмотрим программу со спецификацией в виде тройки Хоара: {P(x)} S {Q(x, y)} [7] . (2.15) Допустим, оператор S является однозначным в области истинности предусловия P(x), а спецификация оператора S является…

Правила корректности для параллельного оператора

Рассмотрим спецификацию параллельного оператора в виде тройки Хоара:

{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.


Математические основы

В данном разделе собраны известные математические понятия, используемые в дальнейшем изложении.

Отношения порядка

· R рефлексивно @ "aÎD. a R a, · R иррефлексивно @ "aÎD. Ø a R a, · R симметрично @ a R b Þ b R a,

Наименьшая неподвижная точка

Пусть F: D→D - произвольная тотальная (т. е. всюду определённая) функция на D. Функция F называется монотонной, если "a,b Î D. a… Лемма 3.2. {Fn(⊥)}n≥0 – для монотонной функции F определяют… Лемма 3.3. Если F монотонна и a0 ⊑ a1 ⊑ a2 ⊑ … – возрастающая цепь, то F(a0) ⊑ F(a1) ⊑…

Математическая индукция

· Начальный шаг: утверждение P(n) доказывается для n = 0 (база индукции); · Индуктивный шаг: утверждение P(n) считается истинным для значения n… Переменная n называется индукционной переменной. Метод математической индукции базируется на аксиоме индукции:

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

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.


Язык исчисления вычислимых предикатов,

Его логическая и операционная семантика

Множество вычислимых формул исчисления предикатов будем рассматривать в качестве общего базиса для всех языков, допускающих построение логической… Язык CCP определяется в качестве минимального ядра для чистых языков…

Структура программы на языке CCP

Программа на языке CCP состоит из набора определений предикатов. Определение предиката A º K сопоставляет вычислимую формулу K определяемому… j(d1, d2, …, dn: e1, e2, …, em) , (4.1) где n ³ 0, m > 0, j - имя предиката или переменной предикатного типа (см. разд. 4.2); d1, d2, …, dn - имена…

Система типов данных

Тип определяет множество значений. Тип идентифицируется именем типа. Система типов языка CCP включает примитивные типы, подмножество произвольного… Примитивными типами являются: логический, целый, вещественный и литерный. Для… Для каждого примитивного типа определены два вида предикатов равенства: =(x: y) и =(x, y: b). Для предиката =(x: y)…

Логическая и операционная семантика языка CCP

LS(j(d: e)) @ j(d, e) . Пусть A(x:y) º K(x:y) - определение предиката (2). Тогда LS(A(x:y) º K(x:y)) @ A(x,y) º LS(K(x:y)) [14] .

Семантика вызова предиката

A(z:u) . (4.12) Здесь A есть имя предиката или имя переменной предикатного типа; z - возможно… A(x:y) º K(x:y) , (4.13)

Оператор суперпозиции

Оператор суперпозиции является правой частью следующего определения предиката:

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 проводится аналогично. □

Конструктор предиката

LS(ConsPred(x, B: A)) @ "y"z. (LS(A(y: z)) º LS(B(x, y: z))) . (4.23) Здесь x, y и z - произвольные непересекающиеся наборы переменных, причем… Допустим, вызов предиката ConsPred(x, B: A) находится в правой части определения некоторого предиката, исполняемого в…

Конструктор массива

LS(ConsArray(x, B: A)) @ "y"z. (LS(A(y: z)) º LS(B(x, y: z))) . (4.27) Здесь x, y и z - произвольные непересекающиеся наборы переменных, причем набор… Логическая семантика ConsArray (4.27) и ConsPred (4.23) идентична, однако отличается исполнение. Пусть вызов…

Программа

Имя определяемого предиката должно быть отлично от имен базисных предикатов, имен других определяемых предикатов, а также от имен типов,… Исполнение программы заключается в исполнении некоторого вызова предиката… s = newSect(z,u); (4.32)

Рекурсивные определения предикатов

Определение предиката B рекурсивно, если истинно отношение def(B, B). Для рекурсивно определяемого предиката B рекурсивным кольцом называется набор… Возможны более сложные формы рекурсии. Предикат B косвенно зависит от C, если… График предиката B(x:y) есть Gr(B) = {(x, y) | LS(B(x:y))}. Как следствие, LS(B(x:y)) º (x, y) Î Gr(B).…

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

Лемма 4.17. Оператор суперпозиции (4.16), параллельный оператор (4.19) или условный оператор (4.20) является однозначным, если вызываемые в… Лемма 4.18. Пусть имеется рекурсивное кольцо предикатов (4.36). Кроме… Доказательство. Из-за ограничений на сложные формы рекурсии предикат, являющийся значением аргумента, не может входить…

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

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. Аргументация в пользу типового языка заключается в том, что указание типов переменных существенно повышает понимание программы.

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

Aj(t, xj: yj) º Pj(t, xj) {Kj(t, xj: yj)} Qj(t, xj, yj); j = 1…n; n > 0 . (5.17) Здесь Pj и Qj – предусловие и постусловие для предиката Aj; t – набор… W(t) º { Pj(t, xj) Þ ($yj. LS(Kj(t, xj: yj))) & (LS(Ki(t, xj: yj)) Þ Qj(t, xj, yj)) }. (5.18) …

Язык предикатного программирования

Введение

Язык предикатного программирования 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 либо какой-либо другой символ, который можно отобразить).

Лексемы

ЛЕКСЕМА ::= ИДЕНТИФИКАТОР | КЛЮЧЕВОЕ-СЛОВО | КОНСТАНТА | ОПЕРАЦИЯ | РАЗДЕЛИТЕЛЬ| МЕТКА ИДЕНТИФИКАТОР ::= НАЧАЛО-ИДЕНТИФИКАТОРА СИМВОЛ-ИДЕНТИФИКАТОРА*

Предикаты

Программа состоит из набора определений предикатов.

Определение предиката

ИМЯ-ПРЕДИКАТА ::= ИДЕНТИФИКАТОР Значением ОПИСАНИЯ-ПРЕДИКАТА является предикат, обозначаемый именем… ОПИСАНИЕ-ПРЕДИКАТА ::= ОПИСАНИЕ-ПРЕДИКАТА-ФУНКЦИИ |

Спецификация предиката

СПЕЦИФИКАЦИЯ-ПРЕДИКАТА ::= ИМЯ-ПРЕДИКАТА ОПИСАНИЕ-СПЕЦИФИКАЦИИ-ПРЕДИКАТА Имя предиката обозначает предикат, представленный описанием спецификации предиката.

Вызов предиката

ВЫЗОВ-ПРЕДИКАТА ::= ВЫЗОВ-ПРЕДИКАТА-ФУНКЦИИ | ВЫЗОВ-ПРЕДИКАТА-ГИПЕРФУНКЦИИ ВЫЗОВ-ПРЕДИКАТА-ФУНКЦИИ ::=

Программа

ОПИСАНИЕ-МОДУЛЯ ::= [ЗАГОЛОВОК-МОДУЛЯ] СПИСОК-ОПИСАНИЙ ЗАГОЛОВОК-МОДУЛЯ ::= module ИМЯ-МОДУЛЯ [ ( ОПИСАНИЯ-АРГУМЕНТОВ ) ]; ИМЯ-МОДУЛЯ ::= ИДЕНТИФИКАТОР

Операторы

БЛОК ::= { ОПЕРАТОР }

ОПЕРАТОР ::= [ОПИСАНИЕ-ПЕРЕМЕННЫХ ;]{ ЗАМКНУТЫЙ-ОПЕРАТОР |

[ОПИСАНИЕ-ПЕРЕМЕННЫХ ;] ПАРАЛЛЕЛЬНЫЙ-ОПЕРАТОР |

[ОПИСАНИЕ-ПЕРЕМЕННЫХ ;] ОПЕРАТОР-СУПЕРПОЗИЦИИ

Описанные переменные считаются локальными в теле предиката. Тип локальной переменной может быть также определен описателем 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. Использование множеств

Массивы

Описание типа массива

array ( ИЗОБРАЖЕНИЕ-ТИПА-ЭЛЕМЕНТА , ИЗМЕРЕНИЯ-МАССИВА ) ИЗОБРАЖЕНИЕ-ТИПА-ЭЛЕМЕНТА ::= ИЗОБРАЖЕНИЕ-ТИПА ИЗМЕРЕНИЯ-МАССИВА ::= ИЗОБРАЖЕНИЕ-ТИПА-ИНДЕКСА [, ИЗМЕРЕНИЯ-МАССИВА]

Вырезка массива

ВЫРАЖЕНИЕ-МАССИВ [ СУЖЕННЫЙ-НАБОР-ТИПОВ-ИНДЕКСОВ ] ВЫРАЖЕНИЕ-МАССИВ ::= ВЫРАЖЕНИЕ СУЖЕННЫЙ-НАБОР-ТИПОВ-ИНДЕКСОВ ::= НАБОР-ИНДЕКСОВ

Определение массива

ОПРЕДЕЛЕНИЕ-ИНДЕКСОВ ОПРЕДЕЛЕНИЕ-ЭЛЕМЕНТА-МАССИВА | АГРЕГАТ-МАССИВ | ОПРЕДЕЛЕНИЕ-МАССИВА-ПО-ЧАСТЯМ

Объединение массивов

ВЫРАЖЕНИЕ-МАССИВ + ВЫРАЖЕНИЕ-МАССИВ являются выражения, значениями которых являются массивы. Объединяемые массивы…

Формулы

ОПИСАНИЕ-ФОРМУЛЫ ::= formula ИМЯ-ФОРМУЛЫ ( ОПИСАНИЯ-АРГУМЕНТОВ [: ТИП-РЕЗУЛЬТАТА] ) = ФОРМУЛА

Процессы

ОПРЕДЕЛЕНИЕ-ПРОЦЕССА ::= process ИМЯ-ПРОЦЕССА [( [ОПИСАНИЯ-АРГУМЕНТОВ] : ОПИСАНИЯ-РЕЗУЛЬТАТОВ-ГИПЕРФУНКЦИИ )]

Императивное расширение

ЗАГОЛОВОК-ПРЕДИКАТА ::= ИМЯ-ПРЕДИКАТА ( [ОПИСАНИЯ-АРГУМЕНТОВ] [: ОПИСАНИЯ-РЕЗУЛЬТАТОВ] ) ВЫЗОВ-ПРЕДИКАТА-ФУНКЦИИ ::=

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

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.


Технология предикатного программирования

Для языка P разрабатывается метод управляемой полуавтоматической трансляции применением последовательности трансформаций, преобразующих предикатную… · склеивание переменных, реализующее замену нескольких переменных одной; · замена хвостовой рекурсии циклом;

Подстановка определения предиката на место вызова

| x | = | e |; { S }; | z | = | y | . (7.1) Конструкции | x |, | z | и | y | являются мультипеременными, а | e | -… Описанная трансформация подстановки определения реализуется другим способом, нежели похожая на нее операция…

Замена хвостовой рекурсии циклом

Существует специальный случай рекурсии, называемый хвостовой рекурсией(tail-рекурсией в языке Лисп [1]), когда можно заменить рекурсию циклом.… · имя вызываемого предиката совпадает с именем определяемого предиката, в… · вызов является последней исполняемой конструкцией в определении предиката, содержащем вызов.

Склеивание переменных

Задача склеивания переменных в данной постановке вряд ли может стать актуальной для оптимизации функциональных программ:в определении функции нет… Склеивание переменных рассматривалось ранее в рамках задачи экономии памяти в… В отличие от задачи экономии памяти [2] склеиванию подлежат только те переменные, между которыми имеется…

Метод обобщения исходной задачи

В качестве адекватной техники программирования предлагается универсальный метод обобщения исходной задачи для получения решения с хвостовой формой… Дадим иллюстрацию метода на примере 5.1 программы умножения через сложение.… УмнO(nat a, b, d: nat c) prea ≥ 0 & b ≥ 0 & d ≥ 0 postc = a * b + d;

Трансформация кодирования структурных объектов

Пример 7.1. Программа суммирования sum(s: c) элементов списка s. Отметим, что более типичной является программа суммирования элементов массива.… Спецификацию программы суммирования определим рекурсивным предикатом:

Пример. Сортировка простыми вставками

Рассмотрим задачу сортировки простыми вставками [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], однако представлен для массивов, а не списков. Использование массивов вместо списков делает алгоритм существенно сложнее. Намного сложнее становится доказательство корректности, поскольку программа представляется логикой второго порядка.

Гиперфункции

elemTwo(list(int) s: int e,bool exist ) (7.12) { if (s = nil Ú s.cdr = nil) exist = false else { e = s.cdr.car || exist = true}

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)

Else break

} }; Подставим определения предикатов взятьЧисло и перваяЦифра на место вызовов. Проведем очевидные упрощения.

Else break

}; Далее, поскольку внутренний цикл в теле предиката Сумма не имеет нормального… СуммаСтроки(string s: nat n) (7.38)

Else break

n = n + v } }

Else break

n = n + v } Можно обнаружить следующий недостаток программы (7.39): если строка s завершается цифрой, то проверка исчерпания…

Заключение

Технология предикатного программирования предоставляет аппарат для доказательства корректности предикатных программ. При наличии спецификации в виде предусловия и постусловия для каждого определяемого предиката корректность предикатной программы может быть доказана строго математически. Используемая техника доказательства базируется на системе правил доказательства корректности для конструкций языка 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, близкой к нулю.

– Конец работы –

Используемые теги: Предикатное, Программирование0.056

Если Вам нужно дополнительный материал на эту тему, или Вы не нашли то, что искали, рекомендуем воспользоваться поиском по нашей базе работ: Предикатное программирование

Что будем делать с полученным материалом:

Если этот материал оказался полезным для Вас, Вы можете сохранить его на свою страничку в социальных сетях:

Еще рефераты, курсовые, дипломные работы на эту тему:

Постановка задачи линейного программирования и двойственная задача линейного программирования.
Всвязи с развитием техники, ростом промышленного производства и с появлением ЭВМвсе большую роль начали играть задачи отыскания оптимальных решений… Именно в силу этого процесс моделированиячасто носит итеративный характер. На… Здесь имеется полная аналогия с тем, как весьма важнаи зачастую исчерпывающая информация о поведении произвольной…

Методы линейного программирования, двойственность в линейном программировании
Методы линейного программирования двойственность в линейном... Задание Задание Задание...

НАДЕЖНОЕ ПРОГРАММНОЕ СРЕДСТВО КАК ПРОДУКТ ТЕХНОЛОГИИ ПРОГРАММИРОВАНИЯ. ИСТОРИЧЕСКИЙ И СОЦИАЛЬНЫЙ КОНТЕКСТ ПРОГРАММИРОВАНИЯ. ИСТОЧНИКИ ОШИБОК В ПРОГРАММНОМ СРЕДСТВЕ
ВВЕДЕНИЕ... Лекция НАДЕЖНОЕ ПРОГРАММНОЕ СРЕДСТВО КАК ПРОДУКТ ТЕХНОЛОГИИ... Программа как формализованное описание процесса обработки данных Программное средство...

Объектно-ориентированное программирование как идеология программирования и как технология. Достоинства и недостатки
Класс это шаблон который определяет форму объекта Он задает как данные так и код который оперирует этими данными Объекты это экземпляры... Объявление объекта типа Building... Building house new Building...

Лабораторная работа №2 по "Основам теории систем" (Решение задач линейного программирования симплекс-методом. Варианты разрешимости задач линейного программирования)
Будем увеличивать , т.к. ее увеличение вызовет большее увеличение функции цели.Предположим, что , тогда Запишем новый опорный план . Все оценки… Теперь базисными переменными являются , а свободными . Для анализа этого плана… Будем увеличивать . Пусть , тогда откуда получаем Все оценки опорного плана должны бытьнеотрицательны, а значит должны…

Лекция 1. Объектно-ориентированное программирование – это новый подход к программированию. Объектно- ориентированные языки обладают свойством
ВВЕДЕНИЕ... Приступая к изучению более сложных конструкций языка С следует прежде всего повторить тот материал который был...

В первом семестре рассматриваются основные конструкции языка Си и базовая технология программирования структурное программирование
В первом семестре рассматриваются основные конструкции языка Си и базовая технология программирования структурное программирование... Структурное программирование это технология создания программ позволяющая... Компиляторы и интерпретаторы Трансляторы бывают...

Введение в нейролингвистическое программирование. Новейшая психология личного мастерства
На сайте allrefs.net читайте: "Введение в нейролингвистическое программирование. Новейшая психология личного мастерства"

Информатика и программирование
Факультет информационных технологий... Учебно методическое пособие...

Основы программирования в среде C++ Builder
Учреждение образования...

0.036
Хотите получать на электронную почту самые свежие новости?
Education Insider Sample
Подпишитесь на Нашу рассылку
Наша политика приватности обеспечивает 100% безопасность и анонимность Ваших E-Mail
Реклама
Соответствующий теме материал
  • Похожее
  • По категориям
  • По работам