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

Сущность формального доказательства заключается в преобразовании кода программы к логической структуре [3, 6] Составляется описание утверждений, которые задают вход–выход программ с помощью логических операторов, а также комбинациями логических переменных (true/false), логическими операциями (конъюнкция, дизъюнкция и др.) и кванторами всеобщности и существования (табл.7.1.).

Таблица 7.1

Логические операции

–––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––

Название Примеры Значение

––––––––––––––––––––––––––––– ––––––––––––––––––––––––––––––––––––––––––

Конъюнкция x & y x и y

Дизъюнкция x * y x или y

Отрицание Øx не x

Импликация x ® y если

х то у

Эквивалентность х = у х

равнозначно у

Квантор всеобщности " х Р(х) для всех х, условие истинно

Квантор существования $ х Р(х) существует х, для которого

Р(х) истина

1. Для примера метода доказательства предлагается к рассмотрению задача сортировки одномерного массива целых чисел Т длины N (Т [1:N]) для получения из него эквивалентного массива Т’

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

Входные условия запишем в виде начального утверждения:

Аbeg: (Т [1:N] – массив целых ) & ( Т' [1:N] массив целых ).

Выходное утверждение Аend запишем как конъюнкции таких условий:

(а)       (Т– массив целых ) & (Т' – массив целых )

(б)      ( " i если i £ N то   $ j (T'( i ) £ T' ( j )))

(в)      ( " i если   i < N

то (T' ( i ) £ T' ( i+1) ),

то есть Аend – это (Т – массив целых ) & (Т'

– массив целых ) &   " i если i £ N то $ j (T'( i ) £ T' ( j )) &   " i если i < N то (T' ( i ) £ T' ( i+1) ).

Для расположения элементов массива Т в порядке возрастания их величин в массиве Т’ в используется алгоритм пузырьковой сортировки, суть которого заключается в предварительном копировании массив Т в массив Т', а затем проводится сортировка элементов согласно условия их возрастания.    Алгоритм сортировки представлен на блок–схеме (рис.7.1).

Операторы алгоритма размещены в прямоугольниках. Условия, с помощью которых происходит выбор альтернативных путей в алгоритме, представлен в параллелограммах. Кружками отмечены точки с начальным Abeg конечным условиями Aend и состояниями алгоритма: кружок с нулем обозначает начальное состояние, кружок с одной звездочкой – состояние после обмена местами двух соседних элементов в массиве Т', кружок с двумя звездочками обозначает состояние после обмена местами всех пар за один проход массива Т'.

Кроме уже известных переменных Т, T' и N, в алгоритме использованы еще два переменные: i – типа целая и М – булева, значением которой являются логические константы true и false.

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

Так оператор присваивания означает, что для всех i (i £ N & i>0 ) выполняется (T' [i] : = T [i]). Результат выполнения алгоритма в точке с нулем может быть выражен утверждением:

(T[1: N] – массив целых) & (T '[1: N] – массив целых)

& ("i если i £ N (T [ i] = T [ i] )).

Доказательство очевидно, поскольку за семантикой оператора присваивания, обеспечивающая поэлементную пересылку чисел из Т в T’ , сами элементы при этом не изменяются и порядок их в Т і T' одинаковый. Получили, что условие (б) исходного утверждения выполнено. Первая строка доказанного утверждения совпадает с условием (а) исходного утверждения Аend и остается справедливой до конца работы алгоритма. В точке алгоритма с одной звездочкой выполняется оператор

(i < N) (T'( i)) > T' (i + 1) ® (T' ( i) и T' (i + 1)    для изменения местами элементов.

В результате работы оператора будет справедливым такое утверждение:

$ i если i < N то (T'(i) < T'(i +1), которое является   частью условия   (в) утверждения Аend

(для одной конкретной пары смежных элементов массива T').

Очевидно, что семантика оператора обмена местами не нарушает условия (б) выходного утверждения Аend.

Abeg T = T’ 0

M =true

i = 0

M=true Aend

Ø M = true

ні

i = i + 1

i < N

ні T’(i)>T’(i+1)

Изменить

T( и) на T(и+1)

M = true

                     Рис.7.1.   Схема сортировки   элементов массива Т'

В точке с двумя звездочками выполнены все возможные операции обмена местами пар смежных элементов массива T' за один проход через T', то есть оператор обмена работал один или больше раз. Однако пузырьковая сортировка не дает гарантии, что достигнуто упорядочение за один проход по массиву T', поскольку после очередного обмена индекс i увеличивается на 1 независимо от того, как соотносится новый элемент T '( i) с предшествующим элементом T '(i – 1).

В этой точке также справедливое утверждение:

$ i , если   i < N то T' ( i) < T' ( i + 1).

Часть алгоритма, обозначенная точкой с двумя звездочками выполняется до тех пор, пока не будет упорядочен весь массив, то есть не будет выполняться условие (в) утверждения Аеnd для всех элементов массива T':

"i, если i < N то T' (i) < T' (i+ 1).

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

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

Другими словами, если первое утверждение – А1 и первая точка преобразования – А2 , то первой теоремой есть: А1   ® А2..

Если А3 есть такой точкой преобразования, то второй теоремой будет: А2 ® А3.

Таким образом, формулируется общая теорема:

Аі ® Аj,где Аі и Аj    – смежные точки преобразования.



Последняя теорема формулируется так, что условие «истинное» в последней точке и отвечает истинности выходного утверждения:     Аk ® Аend.

Соответственно, можно возвратиться потом к точке преобразования Аend    и к

предшествующей точке преобразования. Доказали, что     Аk ® Аend , а значит и Аj ® Аj +1 и так далее, пока не получим, что А1   ® А0

.

Результат любого другого подхода к доказательству правильности будет аналогичный.

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

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

Содержание раздела