Введение в курс предикатного программирования

В представленном учебнике изложен материал лекций по предикатному программированию, которые читались в Новосибирском государственном университете с 2006 по 2009 гг. Данный курс имел два названия: «Формальные методы в описании языков и систем программирования» для студентов 2-го курса магистратуры факультета информационных технологий и «Предикатное программирование» для студентов механико-математического факультета.

Курс начинается общеметодологическим определением понятия программы с рассмотрением двух основных свойств программы: автоматической вычислимости и наличия спецификации. Во втором разделе излагается модель корректности программ для функциональных и императивных программ. Определяется понятие спецификации программы в форме тройки Хоара. Вводится понятие логической семантики. Определяются две системы правил доказательства корректности для оператора суперпозиции, параллельного оператора и условного оператора. В третьем разделе излагаются отдельные положения математической логики: отношения порядка, наименьшая неподвижная точка и метод полной структурной математической индукции. Четвертый раздел описывает язык исчисления вычислимых предикатов CCP (Calculus of Computable Predicates) и его формальную (логическую и операционную) семантику. Для всех конструкций языка и программы в целом доказывается согласованность логической и операционной семантики. Рекурсивные определения предикатов трактуются с использованием аппарата наименьшей неподвижной точки. Язык CCP определяется как минимальное ядро, из которого можно построить любой чистый язык функционального программирования; при этом семантика языка выражается через семантику конструкций ядра. В пятом разделе определяется расширяющаяся цепочка языков CCP Ì P1 Ì P2 Ì P3. Язык P1 получается из CCP применением открытой подстановки определений предикатов на место их вызовов. В языке P2 определяются обобщенные формы оператора суперпозиции и параллельного оператора. Язык P3 определяет набор конструкций, которые в языках императивного программирования соответствуют понятию выражения. Для языков P2 и P3 определяется система правил доказательства корректности новых языковых конструкций. Правила доказательства корректности рекурсивных предикатов определяются в виде правил структурной полной математической индукции.

В шестом разделе в полном объеме описывается последняя версия языка предикатного программирования, оформленная в стиле серии языков C, C++ и др., привычном для подавляющего большинства программистов. В седьмом разделе описываются технология предикатного программирования и методы доказательства корректности предикатных программ. Представлен метод управляемой полуавтоматической трансляции применением последовательности трансформаций, преобразующих предикатную программу в эффективную императивную программу на императивном расширении языка P. Используются трансформации четырех видов: склеивание переменных, реализующее замену нескольких переменных одной; замена хвостовой рекурсии циклом; подстановка определения предиката на место его вызова; кодирование структурных объектов низкоуровневыми структурами с использованием массивов и указателей. Описывается универсальный метод обобщения исходной задачи для получения решения с хвостовой формой рекурсии. Этот метод нередко оказывается ключевым для эффективной реализации предикатных программ. Предлагается языковая конструкция нового вида - гиперфункция, позволяющая гибко декомпозировать программу произвольным образом.