2010 Предикатное программирование Формальные методы в описании языков и систем программирования п/г спецкурс Ведет спецкурс: Шелехов Владимир Иванович, - презентация

1 2010 Предикатное программирование Формальные методы в описании языков и систем программирования п/г спецкурс Ведет спецкурс: Шелехов Владимир Иванович, зав. лаб. Системного программирования ИСИ, к.т.н., р.т , ИСИ СО РАН,

2 Кризис программирования 1960-е Структурное программированиеЭ.Дейкстра Технологии программирования Объектно-ориентированное программирование Языки спецификации программ Формальная верификация программ Доказательное программирование Внедрение формальных (математических) методов в практику программирования. Обучение нового поколения программистов

3 Программа спецкурса общее понятие программы корректность программ с предикатной спецификацией язык исчисление вычислимых предикатов методы доказательства корректности предикатных программ язык и технология предикатного программирования язык спецификации процессов технология спецификации и реализации программ реального времени (реактивных систем)

4 Практика построения спецификаций программ Построение предикатных программ Математическое доказательство корректности предикатных программ Построение эффективных программ методом трансформации Спецификация простых протоколов

5 Лекция 1 Общее понятие программы Автоматическая вычислимость Спецификация программы

6 Алгоритм и программа Программа есть описание алгоритма решения задачи, заданное на языке программирования Формализации понятия алгоритма: машина Тьюринга, частично рекурсивные функции, нормальный алгорифм Маркова и каноническая система Поста Основные свойства программы: автоматическая вычислимость наличие спецификации программы логика программы

7 Автоматическая вычислимость Автоматизация вычислений: счеты арифмометры счетно-решающие устройства ЭВМ калькулятор Программа есть алгоритм, реализованный таким способом и в такой форме, что вычисление алгоритма проводится автоматически

8 Способы реализации программы аппаратно реализованная программа (интегральная микросхема, чип) программа на языке программирования Язык программирования определяет правила представления программы в виде текста в конечном алфавите символов: типы данных структура памяти исполняемой программы виды языковых конструкций программы правила исполнения конструкции каждого вида и программы в целом

9 Процессор языка программирования аппаратно реализованный процессор языка системы команд ЭВМ реализованный на др. языке программирования (интерпретатор байткода для языка Java) виртуальный (трансляция на другой язык) представлен описанием операционной семантики исходного языка

10 Спецификация программы Модель применения программы Спецификация программы описание преобразования информации, реализуемого вычислением программы Базовый процесс окружение программ а

11 Спецификация описывает связь между входными и выходными потоками информации. Связь либо отражает закон природы, выраженный в математической форме, либо является интерфейсом, спроектированным человеком. Язык спецификаций Связь между спецификацией и программой Свойство 1. Спецификация первична по отношению к программе. ДНК ? Свойство 2. Программа должна соответствовать спецификации.

12 Свойство 3. Будучи написанной, программа всегда существует и является строго определенной в силу строгости языка программирования. Спецификация, напротив, может быть нестрогой, неполной, устаревшей, отсутствовать или быть ошибочной. Свойство 4. Программа на языке программирования является абсолютно точной и полной спецификацией самой себя. Свойство 5. Спецификация может быть невычислимой. Программа автоматически вычислима.

13 Формы спецификации программы Предикатная спецификация представима в виде формулы на языке исчисления предикатов высших порядков Процессная спецификация эффект исполнения программы определяется в виде процесса. Модели: машина конечных состояний, сеть Петри, модель CSP Т.Хоара, машина абстрактных состояний Ю.Гуревича Процессорная спецификация описывает функционирование процессора некоторого языка программирования. Формальная семантика математическое описание семантики языка программирования. Виды формальной семантики: операционная, денотационная и аксиоматическая.

14 Классификация программ программы решения задач дискретной и вычислительной математики программы, работающие в режиме реального времени (реактивные системы) большая часть программ системного программирования

15 Структура предикатной спецификации Предикатная спецификация может быть записана в виде формулы на языке исчисления предикатов. Взаимодействие программы с окружением: ввод данных, исполнение программы, вывод результатов. Других взаимодействий с окружением нет. Ввод можно собрать в начале, вывод – в конце Спецификация определяет функцию, отображающую значения входных данных в значения результатов. Предикатная спецификация условие математической задачи, исходными данными которой являются входные данные программы, а неизвестными результаты программы. Алгоритм строится с использованием свойств (утверждений, лемм, теорем), доказуемых из условия задачи строгими математическими методами. Программа реализация алгоритма решения математической задачи.

16 Рис1. Схема построения программы с предикатной спецификацией Спецификация свойстваалгоритмпрограмма Спецификация СвойстваАлгоритм Программа Алгоритм строится с использованием свойств (утверждений, лемм, теорем), доказуемых из условия задачи. Эти свойства определяют логику решения задачи. Программа реализация алгоритма решения математической задачи. В процессе реализации программа оптимизируется привычным образом: используются циклы вместо рекурсии, используются указатели и т.д.

17 Логика программы Логика программы набор предикатов {Q p } на значениях переменных для разных точек p программы 1. Предикат Q p (z) истинен, когда исполнение программы находится в точке p. 2. Если предикат Q p (z) истинен на некотором наборе значений z=z 0, то существует исполнение с такими значениями переменных в точке p. Извлечение логики из программы в целях дедуктивной верификации обычно реализуется на основе формальной семантики языка программирования.

18 Примеры логики программы в начале программы T = true F( 1 x++ 2, y) Q 2 (…x,y…) = Q 1 (…x-1,y…) 1+ 1 x/y 2 +a Q 2 (…x,y,a…) = Q 1 (…x,y,a…) & y 0 При работе с программой во время отладки программист пытается изъять из кода программы необходимую ему часть логики программы. Однако в качестве логики программы он воспринимает логику решения Большинство оптимизирующих преобразований приводят к усложнению (искривлению) логики программы. Для любой, даже простой, императивной программы ее логика оказывается существенно искривленной. Источниками кривизны логики являются, например, такие конструкции, как циклы и указатели переменных.

19 Пример извлечения логики программы int D(int a, b) функция вычисления наибольшего общего делителя (НОД) положительных a и b. x – делитель a divisor(x, a) z 0. x z = a. НОД(c, a, b) divisor2(с, a, b) & x. (divisor2(x, a, b) x c) Логика решения залачи базируется на следующих известных свойствах НОД: a = b НОД(a, a, b) a > b & НОД(c, a, b) НОД(c, a b, b) НОД(c, a, b) НОД(c, b, a) int D(int a, b) // D(a, b, c) {if (a == b) return a; // c = a else if (a < b) return D(a, b a) // D(a, b a, c) else return D(a b, b) // D(a b, b, c) }

20 a = b НОД(a, a, b) a > b & НОД(c, a, b) НОД(c, a b, b) НОД(c, a, b) НОД(c, b, a) int D(int a, b) // D(a, b, c) = {if (a == b) return a; // a = b c = a else if (a < b) return D(a, b a) // a = b & a < b D(a, b a, c) else return D(a b, b) // a = b & a < b D(a b, b, c) } Логика программы: D(a, b, c) = ( a = b c = a) & ( a = b (a < b D(a, b a, c)) & ( a < b D(a b, b, c)) )

21 Извлечения логики для второй программы int D(int a, b) { // D(a, b, c) for ( ; ; ) { if (a == b) return a; // a = b c = a if (a < b) b = b – a // a < b b = b – a else a = a – b // a < b a = a – b } Логика программы для точки в конце тела цикла E(a, b, a, b) = (a < b b = b – a & a = a) & ( a < b a = a – b & b = b) & a = b Итоговая логика программы: true & E(a, b, a 1, b 1 ) & E(a 1, b 1, a 2, b 2 ) & … & E(a r-1, b k-1, a k, b k ) & a k, = b k & c = a k,

22 Язык программирования называется предикатным, если логика любой конструкции Z этого языка может быть определена единственным предикатом LS(Z), истинным после исполнения Z. Функция LS называется логической семантикой языка. Логика предикатной программы совершенно прозрачна: в качестве логики естественно рассматривать саму программу. Языки предикатного программирования находятся на границе между функциональными и логическими языками.