Теория вычислительных процессов
Лекция 8
назад | содержание | вперед

Лекция 8

2.3. Верификация программ

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

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

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

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

Тестирование - процесс выполнения программы с намерением найти ошибку, а не подтвердить правильность программы. Суть его сводится к следующему. Подлежащую проверке программу неоднократно запускают с теми входными данными, относительно которых результат известен заранее. Затем сравнивают полученный машиной результат с ожидаемым. Если во всех случаях тестирования налицо совпадение этих результатов, появляется некоторая уверенность в том, что и последующие вычисления не приведут к ошибочному итогу, т.е. что исходная программа работает правильно.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

из входного утвержденuя следует выведенное утвержденuе.

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

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

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

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

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

2) Выписать входное и выходное утверждения.

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

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

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

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

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

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

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

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

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

Отметим трудности, связанные с методом индуктивных утверждений. Трудно построить “множество основных аксиом, достаточно ограниченное для того, чтобы избежать противоречий, но достаточно богатое для того, чтобы служить отправной точкой для доказательства утверждений о программах” (Э. Дейкстра). Вторая трудность - семантическая, заключающаяся в формировании самих утверждений, подлежащих доказательству. Если задача, для которой пишется программа, не имеет строгого математического описания, то для нее сложнее сформулировать условия верификации.

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

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


2.3.2. Использование утверждений в программах

Утверждения используются для доказательства правильности программ.

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

Исчисление - это метод или процесс рассуждений посредством вычислений над символами. В исчислении предикатов утверждения являются логическими переменными или выражениями, имеющими значение Т - истина или 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 и массив а[l,..., n]. Отсортировать массив, т.е. установить

Пример 2.10. Определить х как максимальное значение массива a[1,..., n].
Определим постусловие:
R: {x=max({y | y e a})}.
Для построения программы следует определить математическое понятие mах. Тогда

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

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

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

{a=A AND b=B}
r := а; {г = а AND а = А AND b = В};
а:=b; {r=a AND a=B AND b=B};
b := г; {а = В AND b = А}.

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

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


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

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

А1. Аксиома присваивания: {R0} х := Е {R}
Неформальное объяснение аксиомы: так как х после выполнения будет содержать значение Е, то R будет истинно после выполнения, если результат подстановки Е вместо x в R истинен перед выполнением. Таким образом, R0 = R(x) при х = Е. Для R0 вводится обозначение: R0 = RхЕ (у Вирта) или Rх->E (у Дейкстры), что означает, что х заменяется на Е.
Аксиома присваивания будет иметь вид: {Rxe} х := Е {R}.
Сформулируем два очевидных правила монотонности.

А2. Если известно: {Q} S {Р} и {Р} => {R}, то {Q} S {R}
АЗ. Если известно: {Q} S {Р} и {R} => {Q}, то {R} S {Р}
Пусть S- это последовательность из двух операторов S1; S2 (составной оператор).
А4. Если известно:{Q} S1 {Р1} и {Р1} S2 {R}, то {Q} S {R}.
Это правило можно сформулировать для последовательности, состоящей из n операторов.
Сформулируем правило для условного оператора (краткая форма).

А5. Если известно:
{Q AND В} S1 {R} и {Q NOT В} => {R},то {Q} if B then S1 {R}.
Правило А5 соответствует интерпретации условного оператора в языке программирования.

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

А6. Если известно:
{Q AND B} S1 {R} и {Q NOT B} S2 {R},то {Q} if B then S1 else S2 {R}.
Сформулируем правила для операторов цикла.
Предусловия и постусловия цикла until удовлетворяют правилу:

А7. Если известно:
{Q AND NOT В} S1 {Q}, то {Q} repeat S1 until В {Q AND NOT В}.
Правило отражает инвариантность цикла. В данном случае единственная операция - это выполнение шага цикла при условии истинности Q вначале.
Предусловия и постусловия цикла while удовлетворяют правилу:

А8. Если известно:
{Q AND В} S1 {Q}, то {Q} while В do S1 {Q AND NOT В}
Правила А7 - А8 используются для аксиоматического представления стра-тегии построения циклов на основе инварианта цикла Р.

Стратегия построения циклов №1.
1. Построить охрану В такую, что Р AND NOT В => R;
2. Построить тело цикла так, чтобы оно уменьшало ограничивающую функцию при сохранении инварианта цикла.

Стратегия построения циклов №2.
1. Стройте охраняемые команды так, чтобы каждая из них приближала цикл к завершению, а соответствующая охрана обеспечивала сохранение инва-рианта.
2. Завершайте процесс создания охраняемых команд, если их создано дос-таточно для доказательства
Р AND NOT ВВ => R.
Правила А1 - А8 можно использовать для проверки согласованности пере-дачи данных от оператора к оператору, для анализа структурных свойств тек-стов программ, для установления условий окончания цикла и для анализа ре-зультатов выполнения программы.

Доказательство.
1. Очевидно, что Q => х = х + у * 0.
2. Применим аксиому А1 к оператору г:= х, тогда получим {х = х + у*0} г:=х {х=г+у*0}
3. Аналогично, применяя А1 к оператору q := 0, получим: {х = г + у*0} q:=0 {x=r+y*q} .
4. Применяя правило А3 к результатам пунктов 1 и 2, получим {Q} г:= х {х=г+у*0} .
5. Применяя правило А4 к результатам пунктов 4 и 3, получим {Q} г:= х; q:=0 {x=r+y*q}
6. Выполним равносильное преобразование х = г + y*q AND y<= г => х = (г - у) + y*(q + 1)
7. Применяя правило А1 к оператору г:= г - у, получим
{х = (r - у) + y*(q + 1)} r:= r- у {х = r+ y*(q+l)}
8. Для оператора q:= q+l аналогично получим {х = r + y*(q + 1) } q := q+l {х = r + y*q}
9. Применяя правило А4 к результатам пунктов 7 и 8, получим
{х = (r - у) + у*( q + 1)} r := r- у; q := q + 1 {х = r + y*q}
10. Применяя правило А2 к результатам пунктов 6 и 9, получим
{x=r+y*q AND y<=r} r:=r-у; q :=q+ 1 {x=r+y*q}
11. Применяя правило А8 к результату пункта 10, получим
{х = r + y*q} whiIe у <= г do begin r:= г - у; q := q + 1 end
{NOT (у <= r) AND (х = r + y*q)} .
Утверждение х = r + y*q является инвариантом цикла, так как значение его остается истинным до цикла и после выполнения каждого шага цикла.
12. Применяя правило А4 к результатам пунктов 5 и 11, получаем то, что требовалось доказать: {Q} S {NOT (у<= r) AND (х = r + y*q)}

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

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


2.4. Вопросы и задания для самоконтроля

2.4. Вопросы и задания для самоконтроля
1. По каким причинам следует заниматься описанием семантики?
2. Каковы основные подходы к спецификации семантики функций?
4. Каковы недостатки операционной семантики?
5. Охарактеризуйте понятие триады Хоара.
6. Поясните смысл понятия «слабейшее предусловие» и его роль в аксио-матической семантике.
7. Докажите (wp(S, R) AND wp(S, NOT R)=F.
8. Приведите пример, показывающий, что утверждение не является ис-тинным во всех состояниях:
(wp(S, R) AND wp(S, NOT R) = Т.
10. Чем отличаются описания смысла программ в операционной семанти-ке, в денотационной семантике, в декларативной семантике и аксиоматической семантике?
11. Какая программа называется правильной?
12. Что проще: доказывать правильность уже существующей программы или использовать идеи доказательства правилънocти во время программирова-ния?
13. В чем заключается смысл верификации пpoграмм?
14. Доказать методом индукции для n >=0 свойство чисел Фибоначчи:

15. Напишите и докажите с помощью метода индуктивных утверждений правильность программы для формирования в лексикографическом порядке и печати всех перестановок из чисел 1, 2, ..., n.
16. Записать на языке логики предикатов, что данный предикат Р(х, у) яв-ляется отношением эквивалентности.
17. Переведите на язык предикатов, используя кванторы, предложение: не-которые элементы массива b[j:k] нулевые.
18. Если fооl (р, t) означает: «Можно обманывать человека в течение вре-мени t», то переведите предложения на язык исчисления предикатов: нельзя обманывать всех людей все время.
19. В чем состоит стратегия построения цикла?
20. Написать программу, используя аксиоматическую стратегию построе-ния и проверки цикла. Дано n > 0. Присвоить переменной х наивысшую сте-пень двойки, не превосходящую n.
Предусловие Q: n >0;
Постусловие R: n < Х <=n < 2*х AND (j: х = 2j);
Инвариант Р: 0< х<= n AND (j: х = 2j);
Ограничение t: n-i.
22. Написать программу, используя различные методы построение инвари-антов циклов. Дан массив B[0 : m-l, 0: n-l], m > 0, n > 0, в котором содержится значение х. Найти вхождение х, при котором х нет в предыдущих строках или в предыдуших столбцах той же строки.


назад | содержание | вперед