Семантическая теория программ

Метод установления правильности программ при помощи строгих средств известен как верификация программ.

В отличие от тестирования программ, где анализируются свойства отдельных процессов выполнения программы, верификация имеет дело со свойствами программ.

В основе метода верификации лежит предположение о том, что существует программная документация, соответствие которой требуется доказать. Документация должна содержать:

? спецификацию ввода-вывода (описание данных, не зависящих от процесса обработки);

? свойства отношений между элементами векторов состояний в выбранных точках программы;

? спецификации и свойства структурных подкомпонентов программы;

? спецификацию структур данных, зависящих от процесса обработки.

К такому методу доказательства правильности программ относится метод индуктивных высказываний, независимо сформулированный К. Флойдом и П. Науром.

Суть этого метода состоит в следующем:

1) формулируются входное и выходное высказывания: входное высказывание описывает все необходимые входные условия для программы (или программного фрагмента), выходное высказывание описывает ожидаемый результат;

2) предполагая истинным входное высказывание, строится промежуточное высказывание, которое выводится на основании семантики операторов, расположенных между входом и выходом (входным и выходным высказываниями); такое высказывание называется выведенным высказыванием;

3) формулируется теорема (условия верификации):

из выведенного высказывания следует выходное высказывание;

4) доказывается теорема; доказательство свидетельствует о правильности программы (программного фрагмента).

Доказательство проводится при помощи хорошо разработанных математических методов, использующих исчисление предикатов первого порядка.

Условия верификации можно построить и в обратном направлении, т.е., считая истинным выходное высказывание, получить входное высказывание и доказывать теорему: из входного высказывания следует выведенное высказывание.

Такой метод построения условий верификации моделирует выполнение программы в обратном направлении. Другими словами, условия верификации должны отвечать на такой вопрос: если некоторое высказывание истинно после выполнения оператора программы, то, какое высказывание должно быть истинным перед оператором?

Построение индуктивных высказываний помогает формализовать интуитивные представления о логике программы. Оно и является самым сложным в процессе доказательства правильности программы. Это объясняется, во-первых, тем, что необходимо описать все содержательные условия, и, во-вторых, тем, что необходимо аксиоматическое описание семантики языка программирования.

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

Таким образом, алгоритм доказательства правильности программы методом индуктивных высказываний представляется в следующем виде:

1) Построить структуру программы.

2) Выписать входное и выходное высказывания.

3) Сформулировать для всех циклов индуктивные высказывания.

4) Составить список выделенных путей.

5) Построить условия верификации.

6) Доказать условие верификации.

7) Доказать, что выполнение программы закончится.

Этот метод сравним с обычным процессом чтения текста программы (метод сквозного контроля). Различие заключается в степени формализации.

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

Для автоматизированной диалоговой системы программист должен задать индуктивные высказывания на языке исчисления предикатов. Синтаксис и семантика языка программирования должны храниться в системе в виде аксиом на языке исчисления предикатов. Система должна определять пути в программе и строить условия верификации.

Основной компонент доказывающей системы - это построитель условий верификации, содержащий операции манипулирования предикатами, алгоритмы интерпретации операторов программы. Вторым компонентом системы является подсистема доказательства теорем.

Отметим трудности, связанные с методом индуктивных высказываний. Повторим, что трудно построить «множество основных аксиом, достаточно ограниченное для того, чтобы избежать противоречий, но достаточно богатое для того, чтобы служить отправной точкой для доказательства высказываний о программах». Вторая трудность - семантическая, заключающаяся в формировании самих высказываний, подлежащих доказательству. Если задача, для которой пишется программа, не имеет строгого математического описания, то для нее сложнее сформулировать условия верификации.

Перечисленные методы имеют одно общее свойство: они рассматривают программу как уже существующий объект и затем доказывают ее правильность.

Метод, который сформулировали К. Хоар и Э. Дейкстра основан на формальном выводе программ из математической постановки задачи.

10.Использование высказываний в программах

Высказывания используются для доказательства правильности программ. Тогда высказывания необходимо формулировать в некоторой формальной логической системе. Обычно используется исчисление предикатов первого порядка.

Исчисление - это метод или процесс рассуждений посредством вычислений над символами. В исчислении предикатов высказывания являются логическими переменными или выражениями, имеющими значение T - истина или F - ложь. Наша цель - при написании программы некоторым способом доказать истинность высказывания (2.2) - триады Хоара {Q} S {R}. Для этого нужно уметь записывать его в исчислении предикатов и формально доказывать его истинность.

Предикат, помещенный в программу, был нами назван высказыванием. Утверждается, что он истинен в соответствующий момент выполнения программы. В предусловии Q нужно отражать тот факт, что входные переменные получили начальные значения. Для обозначения начальных значений будем использовать большие буквы.

Пример 2.8. Пусть надо определить приближенное значение квадратного корня: s = sqrt(n), где n, s Nat. Определим постусловие в виде:

R: sЧs n < (s+1)Ч(s+1).

Пример 2.9. Даны целочисленные n > 0 и массив a[1,...,n]. Отсортировать массив, т.е. установить

R: (? i: 1 i < n: a[i] a[i+1]).

Пример 2.10. Определить x как максимальное значение массива a[1,...,n]. Определим постусловие:

R: {x = max({y | y a})}.

Для построения программы следует определить математическое понятие max. Тогда

R: {(? i: 1 i n: x = a[i]) AND (? i: 1 i n: a[i] = x)}.

Пример 2.11. Пусть имеем программу S обмена значениями двух целых переменных a и b. Сформулируем входное и выходное высказывания программы и представим программу S в виде предиката:

{a = A AND b = B} S {a = B AND b = A}, (2.4)

где A, B - конкретные значения переменных a, b.

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

{a = A AND b = B};

r := a; {r = a AND a = A AND b = B};

a := b; {r = a AND a = B AND b = B};

b := r; {a = B AND b = A}.

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

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

11.Правила верификации К. Хоара

Сформулируем правила (аксиомы) К.Хоара, которые определяют предусловия как достаточные предусловия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к желаемым постусловиям.

A1. Аксиома присваивания: {Ro} x := Е {R}

Неформальное объяснение аксиомы: так как x после выполнения будет содержать значение Е, то R будет истинно после выполнения, если результат подстановки Е вместо x в R истинен перед выполнением. Таким образом, Ro = R(x) при x = E. Для Ro вводится обозначение: Ro = RxЕ (у Вирта) или Rx>Е (у Дейкстры), что означает, что x заменяется на Е.

Аксиома присваивания будет иметь вид:{RxЕ} x := Е {R}.

Сформулируем два очевидных правила монотонности.

A2. Если известно: {Q} S {P} и {P} => {R}, то {Q} S {R}.

A3. Если известно: {Q} S {P} и {R} => {Q}, то {R} S {P}.

Пусть S - это последовательность из двух операторов S1; S2 (составной оператор).

A4. Если известно:{Q} S1 {P1} и {P1} S2 {R}, то {Q} S {R}.

Это правило можно сформулировать для последовательности, состоящей из n операторов.

Сформулируем правило для условного оператора (краткая форма).

A5. Если известно:

{Q AND B} S1 {R} и {Q NOT B} => {R}, то {Q} if B then S1 {R}.

Правило A5 соответствует интерпретации условного оператора в языке программирования.

Сформулируем правило для альтернативного оператора (полная форма условного оператора).

A6. Если известно:

{Q AND B} S1 {R} и {Q NOT B} S2 {R}, то {Q} if B then S1 else S2 {R}.

Сформулируем правила для операторов цикла.

Предусловия и постусловия цикла until удовлетворяют правилу:

A7. Если известно:

{Q AND NOT B} S1 {Q}, то {Q} repeat S1 until B {Q AND NOT B}.

Правило отражает инвариантность цикла. В данном случае единственная операция - это выполнение шага цикла при условии истинности Q вначале.

Предусловия и постусловия цикла while удовлетворяют правилу:

A8. Если известно:

{Q AND B} S1 {Q} , то {Q} while B do S1 {Q AND NOT B}

Правила A1 - A8 можно использовать для проверки согласованности передачи данных от оператора к оператору, для анализа структурных свойств текстов программ, для установления условий окончания цикла и для анализа результатов выполнения программы.

Пример 2.12. Пусть надо определить частное q и остаток r от деления x на y.

Входные данные x, y и выходные данные q, r Nat, причем y > 0.

Задать(x,y); /* x,y получают конкретные значения X,Y */

r := x; q := 0;

while y r do

begin

r := r - y; q := q + 1

end;

выдать(q,r);

Сформулируем постусловие R: (r < y) AND (x = y*q + r).

Нужно доказать, что {y > 0 AND x/y} S {(r < y) AND (x = y*q + r)}.

Доказательство.

1. Очевидно, что Q => x = x + y*0.

2. Применим аксиому A1 к оператору r := x, тогда получим

{x = x + y*0 } r := x {x = r + y*0}.

3. Аналогично, применяя A1 к оператору q := 0, получим:

{x = r + y*0} q := 0 {x = r + y*q}.

4. Применяя правило A3 к результатам пунктов 1 и 2, получим

{Q} r := x {x = r + y*0}.

5. Применяя правило A4 к результатам пунктов 4 и 3, получим

{Q} r := x; q := 0 {x = r + y*q}.

6. Выполним равносильное преобразование

x = r + y*q AND y r => q = (r - y) + y*(q + 1).

7. Применяя правило A1 к оператору r := r - y, получим

{x = (r - y) + y*(q + 1)} r := r - y {x = r+ y*(q+1)}.

8. Для оператора q := q + 1 аналогично получим

{x = r + y*(q + 1)} q := q + 1 {x = r + y*q}.

9. Применяя правило A4 к результатам пунктов 7 и 8, получим

{x = (r - y) + y*(q + 1)} r := r - y; q := q + 1 {x = r + y*q}.

10. Применяя правило A2 к результатам пунктов 6 и 9, получим

{x = r + y*q AND y r} r := r - y; q := q + 1 {x = r + y*q}.

11. Применяя правило A8 к результату пункта 10, получим

{x = r + y*q} while y r do begin r := r - y; q := q + 1 end

{NOT (y <= r) AND (x = r + y*q)}.

Высказывание x = r + y*q является инвариантом цикла, так как значение его остается истинным до цикла и после выполнения каждого шага цикла.

12. Применяя правило A4 к результатам пунктов 5 и 11, получаем то, что требовалось доказать:

{Q} S {NOT (y r) AND (x = r + y*q)}.

Осталось доказать, что выполнение программы заканчивается.

Доказывать будем от противного, т.е. предположим, что программа не заканчивается. Тогда должна существовать бесконечная последовательность значений r и q, удовлетворяющая условиям

1) y r;

2) r, q Nat.

Но значение r на каждом шаге цикла уменьшается на положительную величину: r := r - y (y > 0). Значит, последовательность значений r и q является конечной, т.е. найдется такое значение r, для которого не будет выполняться условие y r и циклический процесс завершится.

12.Основные выводы и результаты

Операционная семантика, сводится к описанию смысла программы посредством выполнения ее операторов на реальной или виртуальной машине.

Операционная семантика является эффективной до тех пор, пока описание языка остается простым и неформальным. Она зависит от алгоритмов, а не от математики.

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

Аксиоматическое определение семантики оператора дается в виде правила, описывающего, как для любого заданного постусловия R можно вывести соответствующее слабейшее предусловие wp(S, R).

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

Основная теорема инвариантности для цикла:

(P AND wp(DO, T)) => wp(DO, P AND NOT BB).

Аксиоматическая семантика является мощным инструментом для исследований в области доказательств правильности и анализа программ. Однако ее полезность при описании содержания языков программирования весьма ограничена. Трудно построить «множество основных аксиом, достаточно ограниченное для того, чтобы избежать противоречий, но достаточно богатое для того, чтобы служить отправной точкой для доказательства высказываний о программах» (Э. Дейкстра).

Денотационная семантика, опирающаяся на теорию рекурсивных функций, основной концепцией имеет определение для каждой сущности языка некоего математического объекта и некоей функции, отображающей экземпляры этой сущности в экземпляры этого математического объекта. Поскольку объекты определены строго, то они представляют собой точный смысл соответствующих сущностей.

Денотационную семантику программы можно определить в терминах изменений состояний идеального компьютера. Изменения состояний в денотационной семантике определяются строгими математическими функциями, а не запрограммированными алгоритмами, как в операционной семантике.

Денотационные описания достаточно сложны, но они дают великолепный метод краткого описания языка.

Декларативная семантика применяется в языках логического программирования, в которых программы состоят из объявлений, а не из операторов. Эти объявления являются высказываниями (операторами в символьной логике).

Декларативная семантика значительно проще, чем семантика императивных языков. Она не требует для проверки отдельного оператора рассмотрения его контекста, локальных объявлений или последовательности выполнения программы.

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

Верификация программ позволяет при помощи строгих средств устанавливать их правильность. При этом используются свойства программы, а не свойства ее отдельных процессов, как при тестировании.

Процесс доказательства на основе метода индуктивных высказываний Флойда и Наура настолько формализуем, что может выполняться на вычислительной машине.

Метод верификации Хоара и Дейкстры основан на формальном выводе программ из математической постановки задачи на основе исчисления предикатов первого порядка.

Правила верификации Хоара определяют достаточные предусловия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к желаемым постусловиям.

Контрольные вопросы и задания

1. По каким причинам следует заниматься описанием семантики?

2. Каковы основные подходы к спецификации семантики функций?

3. Функции F(n) и G(n) определены с помощью операционной семантики равенствами: F(0) = 1, G(0) = 2, F(n) = G(n-1), G(n) = F(n-1) + G(n-1). Найти значения F(3) и G(3).

4. Каковы недостатки операционной семантики?

5. Вычислить высказывания в обоих состояниях

Таблица 2

6. Переведите предложения на язык логики высказываний: «Если дождь будет лить как из ведра, то будь я проклят, купаться не пойду», «Если, когда я буду купаться, дождь будет лить как из ведра, то будь я проклят», «Будет или не будет дождь, я пойду купаться», «Если будет дождь, я не пойду купаться».

7. Доказать закон тождества, используя правила подстановки и транзитивности,

8. Упростить высказывание (((x (z AND y)) (NOTy NOT x)) NOTy).

9. Записать на языке высказываний, что данный предикат P(x, y) транзитивен.

10. Переведите на язык высказываний, используя кванторы, предложение: «Некоторые элементы массива b[j:k] нулевые».

11. Если fool(p, t) означает: «Можно обманывать человека в течение времени t», то переведите предложения на язык исчисления предикатов: «Нельзя обманывать всех людей все время».

12. Охарактеризуйте понятие триады Хоара.

13. Поясните смысл понятия «слабейшее предусловие» и его роль в аксиоматической семантике.

14. Докажите (wp(S, R) AND wp(S, NOT R) = F.

15. Приведите пример, показывающий, что высказывание

(wp(S, R) AND wp(S, NOT R) = Т

не является истинным во всех состояниях.

16. Чем отличаются описания смысла программ в операционной семантике, в денотационной семантике, в декларативной семантике и аксиоматической семантике?

17. Какая программа называется правильной?

18. Что проще: доказывать правильность уже существующей программы или использовать идеи доказательства правильности во время программирования?

19. В чем заключается смысл верификации программ?

20. Рекуррентное правило вычисления чисел Фибоначчи: fn+1 = fn + fn-1, f0 = 0, f1 = 1. Доказать методом индукции для n -- 0 свойство чисел Фибоначчи:

f02 + f12 + … + fn2 = fn fn+1.

21. Напишите и докажите с помощью метода индуктивных высказываний правильность программы для формирования в лексикографическом порядке и печати всех перестановок из чисел 1, 2, …, n.

Размещено на Allbest.ru