01.10.09 Лекция 2 Предикатное программирование 2. Постановка задачи дедуктивной верификации Программа в виде тройки Хоара, однозначность программы, тотальность. - презентация

1 Лекция 2 Предикатное программирование 2. Постановка задачи дедуктивной верификации Программа в виде тройки Хоара, однозначность программы, тотальность и однозначность спецификации Тотальная корректность программы Теорема тождества спецификации и программы 3.Язык исчисления вычислимых предикатов Структура программы на языке CCP Система типов данных

2 Основные свойства программы: автоматическая вычислимость наличие спецификации программы логика программы Свойство 2. Программа должна соответствовать спецификации.

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

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

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

6 2. Постановка задачи дедуктивной верификации для класса программ с предикатной спецификацией

7 Программа – оператор S(x, y) x аргументы набор входных данных, y результаты набор выходных данных. Предикатная спецификация программы формула P(x) & Q(x, y) P(x) предусловие, истинное перед исполнением программы, Q(x, y) постусловие, истинное после исполнения программы. Спецификация изображается в виде: [ P (x), Q(x, y) ] Программа со спецификацией представляется тройкой Хоара {P(x)} S(x, y) {Q(x, y)}.

8 P(x) { S (x, y) k } Q(x, y) (2.1) k – маркер, обозначающий точку k в конце программы L k (x, y) – логика программы в конце программы. Однозначность программы S(x, y) : P(x) & L k (x, y 1 ) & L k (x, y 2 ) y 1 = y 2 Однозначность спецификации [P(x), Q(x, y)] : P(x) & Q(x, y 1 ) & Q(x, y 2 ) y 1 = y 2 Тотальность спецификации [P(x), Q(x, y)] : P(x) y. Q(x, y) Свойство 2. Программа должна соответствовать спецификации. Конкретизация закона соответствия программы и спецификации: - аргументы x должны соответствовать предусловию P(x) перед исполнением программы; - аргументы x и результаты y должны удовлетворять постусловию Q(x, y) после завершения исполнения программы.

9 P(x) { S (x, y) k } Q(x, y) (2.1) Непосредственная экспликация закона соответствия спецификации и программы: P(x) & (L k (x, y) Q(x, y) ) (2.2) Предусловие P(x) не следует из L k (x, y). Оно должно быть доказано ранее – перед вызовом S(x, y). Здесь же оно должно быть истинно априори, и поэтому должно быть посылкой, т.е.: P(x) & L k (x, y) Q(x, y) (2.3) Данное условие определяет частичную корректность программы S (x, y). Условие завершения программы: P(x) y. L k (x, y) (2.4) Тотальная корректность программы S(x, y) относительно спецификации [P(x), Q(x, y)] складывается из частичной корректности и условия завершения программы: P(x) [L k (x, y) Q(x, y)] & y. L k (x, y) (2.5) Частичная корректность Условие завершения программы

10 P(x) & L k (x, y) Q(x, y) (2.3) P(x) y. L k (x, y) (2.4) Термин «корректность» далее используется в смысле тотальной корректности. Лемма 2.1. Если программа корректна относительно спецификации, то спецификация тотальна. Доказательство. Пусть истинно P(x). Необходимо доказать истинность y. Q(x, y). Из условия (2.4) следует истинность y. L k (x, y). Допустим, истинность этой формулы реализуется для некоторого y 0. Из условия (2.3) получаем истинность Q(x, y 0 ), а значит и y. Q(x, y).

11 Предикат A(x, y) является однозначным в области X, если: x X. A(x, y 1 ) & A(x, y 2 ) y 1 = y 2 Лемма 2.2. Допустим, предикат D(x, y) является однозначным в области X, а предикат Z(x, y) тотальный в области X. Пусть истинна формула x X. Z(x, y) D(x, y). Тогда истинна следующая формула: x X. D(x, y) Z(x, y). Как следствие, предикаты D и Z оказываются тождественными в области X. Доказательство. Пусть истинно D(x, y) для некоторого x X. Докажем истинность Z(x, y). Поскольку предикат Z тотальный, то существует некоторый y, для которого истинно Z(x, y). Из Z(x, y) D(x, y) получаем истинность D(x, y). Поскольку истинны D(x, y) и D(x, y), то из однозначности D следует y = y. Тогда истинно Z(x, y).

12 Теорема 2.1 тождества спецификации и программы P(x) { S (x, y) k } Q(x, y) (2.1) Оператор S(x, y) является однозначным, а спецификация [P(x), Q(x, y)] тотальной. Пусть истина формула: P(x) & Q(x, y) L k (x, y) (2.6) Тогда программа (2.1) является корректной. Доказательство. Достаточно доказать (2.5), т.е.: P(x) [L k (x, y) Q(x, y)] & y. L k (x, y) (2.5) Пусть предусловие P(x) истинно. Докажем истинность y. L k (x, y). Из тотальности спецификации следует y. Q(x, y). Пусть эта формула истинна для некоторого y. Тогда из (2.6) истинна L k (x, y) и, следовательно, y. L k (x, y).

13 Докажем истинность формулы L k (x, y) Q(x, y). Поскольку истинны P(x) и формула (2.6), то истинна формула Q(x, y) L k (x, y). В соответствии с леммой 2.2 истинна формула L k (x, y) Q(x, y), поскольку постусловие Q(x, y) тотально, а L k (x, y) однозначно. Лемма 2.8. В условиях теоремы 2.1 истинна ф-ла: P(x) (L k (x, y) Q(x, y)) Доказательство. Допустим, предусловие P(x) истинно. Истинность формулы L k (x, y) Q(x, y) установлена при доказательстве теоремы 2.1. Обратная импликация следует из (2.16). Следствие леммы 2.8: спецификация [P(x), Q(x, y)] является однозначной.

14 Лемма 2.9. Допустим, программа (2.1) является корректной, а ее спецификация однозначной. Тогда истинна формула (2.6), т.е. L k (x, y) выводима из спецификации. Доказательство. Допустим, истинны P(x) и Q(x, y). Докажем истинность L k (x, y). Из корректности программы (2.1) по формуле (2.5) следует истинность формулы L k (x, y) Q(x, y), а также тотальность L k (x, y). Пусть для некоторого y истинно L k (x, y). Тогда истинно Q(x, y), а из однозначности Q следует y = y. Следовательно, истинно L k (x, y).

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

16 Исчисление вычислимых предикатов множество вычислимых формул языка исчисления предикатов язык CCP (Calculus of Computable Predicates) ядро для построения языка предикатного программирования

17 Структура программы на языке CCP Программа набор определений предикатов Определение A K предикат A, оператор K параллельный оператор, оператор суперпозиции, условный оператор Вызов предиката (d 1, d 2, …, d n : e 1, e 2, …, e m )(3.1) φ имя предиката или переменной предикатного типа, n 0, m > 0, d 1, d 2, …, d n имена переменных аргументы вызова, e 1, e 2, …, e m результаты вызова Вычисление предиката Вызов φ(d: e), где d = d 1, d 2, …, d n, e = e 1, e 2, …, e m – наборы переменных n = 0 – вызов предикта соответствует константе Значение φ(d) φ(d: b), где b переменная логического типа Определение предиката A(x: y) K(x: y)(3.2) A имя предиката; набор x аргументы предиката, набор y результаты предиката, K(x: y) – оператор. Предикат – определяемый, базисный, значение переменной. Тип данных определяет набор базисных предикатов со значениями типа Система типов определяет совокупность всех базисных предикатов

18 Тип множество значений, имя типа Система типов: примитивные типы, подмножество типа и структурные типы Примитивные типы: логический BOOL, целый INT, вещественный REAL и литерный CHAR. Базисные предикаты: +(x, y: z) z = x + y, -(x, y: z) z = x - y, -(x: y) y = -x,

19 Предикаты ConsIntZero( : x) x = 0 ConsIntOne( : x) x = 1 x переменная типа T, d возможно пустой набор переменных – параметров типа Подмножество типа T на базе предиката P(x, d) S = Subset(T, x, P, d) = {x T | P(x, d)} (3.3) Subset стандартное имя, P вычислимый, d параметры типа NAT = Subset(INT, x, GE0) = {x INT | x 0}. DIAP(n) = Subset(INT, x, IN1_n, n) = {x INT | x 1 x n}

20 Структурный тип композиция компонентных типов Структурные типы: произведение типов (кортеж), объединение типов, множество подмножеств типа, предикатный тип (в т.ч. массив). Базисные предикаты конструкторы, деструкторы и другие операции Конструктор по значениям компонентных типов строит значение структурного типа. Деструктор для значения структурного типа определяет соответствующие значения компонент. Нет типов указателей !

21 Произведение типов Z = X Y = {(x, y) | x X, y Y} (3.4) x X, y Y, z Z Конструктор ConsStruct(x, y: z) z = (x, y) Деструктор CompStruct(z: x, y) z = (x, y) Объединение типов Z = X + Y = {(1, x) | x X} {(2, y) | y Y} (3.5) Первая компонента (1 или 2) тег значения Конструктор ConsUnion1(x: z) z = (1, x). Конструктор ConsUnion2(y: z) z = (2, y) Деструктор CompUnion(z: i, x, y) либо z = (1, x) и i = 1, либо z = (2, y) и i = 2. Если i = 1, то y не определено. Если i = 2, то x не определено

22 Множество подмножеств конечного типа X: Z = Set(X) = {z | z X} (3.6) Конструктор ConsSetEmpty( : z) z = Конструктор ConsSetElem(x : z) z = {x} Предикат CompSet(z, x: b) b = x z Предикатный тип Z = Pred(D: E) = { (d: e) | d D, e E, - вычислимый } (3.7) множество вычислимых предикатов вида (d: e) для непересекающихся списков переменных d и e Z = { (d: e) | d D, e E, CCP} Конструктор предиката ConsPred будет определен позже Z тип массива D не пуст & типы D конечны & Z d D e (d: e) (d: e) массив с индексом d и элементом массива e Конструктор предиката ConsArray будет определен позже Деструктор CompArray(a, i: x) x = a(i) a(i: x)

23 Произвольный тип либо примитивный, либо вводится следующим определением: = Z = Subset(T, x, P, d) (3.3) Z = X Y (3.4) Z = X + Y(3.5) Z = Set(X) (3.6) Z = Pred(D: E) (3.7) Z, T, X, Y, D, E имена типов, примитивных или определяемых.

24 Тип подмножество типа может быть параметризован набором переменных d Структурный тип параметризован, если параметризован один из его компонентных типов. В качестве параметра может выступать также имя типа. Если, встречающееся в правой части определения типа, не есть имя примитивного типа и этот тип не объявлен как параметр, то должно существовать определение для этого типа Замкнутая совокупность определений типов любой встречающийся тип либо является примитивным, либо имеет определение, либо считается параметром для некоторых типов из совокупности определений Рекурсивный тип определение типа прямо или косвенно, через совокупность определений, использует этот тип

25 Примеры рекурсивных типов Специальный тип NIL = { nil }; nil обозначает пустую последовательность Тип последовательности, составленной из элементов типа T: Seq(T) = NIL + (T Seq) Тип списка LIST для языка Лисп: LIST = Seq(ATOM) ATOM = NIL + NUM + SYMBOL + LIST NUM = INT + REAL SYMBOL = STRING STRING = Seq(CHAR)