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

Используя приведенные выше правила и аксиомы, можно осуществлять доказательство правильности программ. Рассмотрим следующую программу:

2. declare X;

3. declare R; /* R=A*B */

4. declare A,B; /* B0 */

7. do while (X0);

11. end MULTIPLY;

Входным утверждением является предикат B ≥ 0, выходное утверждение R = A×B.

Общая схема доказательства правильности программы:

• B ≥ 0>R = 0 R = 0 по аксиоме присваивания;
• B ≥ 0>R = 0 R = 0 по правилу следствия в связи с тем, что истинны следующие утверждения:

B ≥ 0  (B ≥ 0 R = = 0 истинно.

Необходим инвариант для предиката P цикла do while. Этот инвариант должен описывать работу, выполняемую циклом. В нашем случае цикл вычисляет произведение; таким образом, инвариантом может быть R = A×(B – X). В соответствии с аксиомой цикла, если можно показать, что это выражение инвариантно относительно цикла и что оно истинно, когда цикл заканчивается, то возникает следующая ситуация:

Урок №25. EveryCircuit — Лучшая программа для эмуляции схем.

Таким образом, если выражение R = A×(B – X) (X = 0), а это приводит к истинности соотношения R = A×B, что и требовалось доказать. Следовательно, для того, чтобы завершить доказательство, нужно, чтобы выражение R = A×(B – X) в строке 7 было истинно и оно является инвариантом цикла.

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

Объединение строк 8 и 9 в соответствии с аксиомой следования дает выражение R = A×(B – X)> R = R + A; X = X – 1 R= = A×(B – X)>, которое является желаемым инвариантом соотношения.

Теперь следует показать, что инвариантное выражение в строке 7 истинно, а это эквивалентно доказательству с помощью правил следования следующей теоремы: X = B B ≥ 0 истинно в строке 6  R = A×(B – X).

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

• Доказательства длинны и сложны даже для простой программы.
• Если оперировать нецелочисленными данными, то формулировка аксиом становится затруднительной. Операции со строками, плавающей точкой, доступ к базам данных вызывают серьезные осложнения при аксиоматическом подходе.
• Даже для относительно простого случая — использования целочисленных данных — существуют трудности. Например, все ЭВМ используют слова фиксированной длины для записи целых чисел. Возможно переполнение разрядной сетки, и аксиомы должны учитывать эти условия.
• Реальные языки программирования имеют встроенные структуры, которые нелегко поддаются проверке на правильность.

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

Лекция 73: Реализация функции бинарного поиска на языке C с доказательством правильности программы

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

Источник: studfile.net

Доказательство правильности программ. Структурное программирование

2. Пример использования структурного программирования

Структу́рное программи́рование — методология разработки программного
обеспечения, в основе которой лежит представление программы в виде
иерархической структуры блоков. Предложена в 1970-х годах Э. Дейкстрой
Структурное программирование:
1. Проектирование сверху вниз
2. Функциональное программирование
3. Структурное кодирование
Задача нахождения НОД.
I. Общая постановка: даны целые a и b, найти их НОД.
Пусть a и b ≠ 0 и есть НОД(a,b). Ноль делится на любое число, поэтому
НОД(0, 0) = 0 и
НОД(u, v) = НОД(v, u) и
НОД(u, v) = НОД (-u, v) и
НОД(u, 0) = u
II. Даны целые, неотрицательные a и b, найти их НОД.
Проведем декомпозицию этой задачи. Предположим, что можно привести
задачу нахождения НОД(a,b) для b > 0, к задаче нахождения
НОД(x,y), где x и y тоже неотрицательные и y < b. Тогда после
выполнения такого преобразования конечное число раз, придем к
ситуации, когда y = 0. С учетом соотношений получим
НОД(a, b) = НОД (x, y) = x

3. Пример использования структурного программирования

Декомпозиция на три подзадачи:
1) положить x = a и y = b
2) если y ≠ 0, то а) уменьшить y и изменить x так, чтобы x и y
оставались >= 0, и чтобы значение НОД(x,y) оставалось тем же.
b) повторить второй этап
3) если y = 0, положить НОД(a,b) = x
Первая и третья задача уже достаточно просты, а вторая …решена
Евклидом:
III. Если (x div y) – целая часть, а (x mod y) – остаток, то
x = (x div y) * y + (x mod y)
и если x и y делятся на какое-то число, то на это число будет
делиться y и x – (x div y) * y, то есть y и (x mod y)
и НОД(x, y) = НОД(y, x mod y),
так как (x mod y) < y, эти рассуждения показывают как «уменьшить» y
и «изменить» x во второй подзадаче. Алгоритм:
1) положить x = a и y = b
2) если y ≠ 0, то
а) установить r = x mod y b) положить x = y с) положить y = r.
d) повторить второй этап
3) если y = 0, положить НОД(a,b) = x

4. Пример использования структурного программирования

• В исходной постановке задачи только входные данные a и b, мы
ввели в рассмотрение три переменные: x, y и r >= 0 …..
Представим этапы проектирования блок-схемами…
1.
— a>0, b>=0
2.
— a>0, b>=0
Найти НОД(a, b)
положить x = a и y = b
—НОД(a, b) = x
— НОД(a, b)= НОД(x, y)
y≠0
нет
НОД(a, b)= НОД(x, y) —да
уменьшить Y и изменить x
с сохранением НОД
— НОД(a, b) = x

5. Пример использования структурного программирования

3.
— a>0, b>=0
положить x=a
положить y = b
— НОД(a, b ) = НОД(x, y)
y≠0
нет
да
НОД(a, b)= НОД(x,y)
— НОД(a, b) = x
r = x mod y
x=y
y=r
Это процесс декомпозиции.
Способы композиции действий, составляющих алгоритм:
линейная, итерационная.
Продолжение декомпозиции – положить r = x mod y:

6. Получение целой части и остатка отделения

—x ≥ 0, y > 0
положить q = 0
положить r =x
— x = q*y + r, r ≥ 0
r≥y
нет
x = q*r + y, r ≥ 0—
да
x = q*y+r, r ≥y
положить r = r – y
положить q = q + 1
—x = q*y+r, 0 ≤ r < y

7. Статическая и динамическая структура программы

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

8. Спецификация программы и правила вывода

Любой оператор или изменяет состояние вычислений… или
анализирует и принимает решение…
Любой язык программирования включает в себя некоторое
количество простых операторов и методы объединения,
композиции их в составные, структурные.
Задача: описать соотношения и правила вывода, которые
позволят определить эффект воздействия простого оператора
на состояние вычислений и выделить свойства составного
оператора из свойств входящих в него простых операторов.
На структурной схеме нахождения div и mod определены
состояния вычислений с помощью соотношений, которые
должны выполняться для входных и промежуточных величин.
Фундаментальным свойством всех способов композиции является
возможность объединения в одну сложную структурную схему с
одним входом и одним выходом произвольного количества
любых структурных схем.

9. Спецификация программы и правила вывода

Спецификация программы:
< P>S < Q >(1)
-P
S
-Q
Если соотношение P – истинно перед выполнением S, то после
завершения выполнения S, будет истинно выражение Q. …
Если S — это программа, корректность которой мы должны
установить, то необходимо доказать нотацию (1), где P –
соотношение, которому должны удовлетворять входные
данные, а Q – выходные.
Для задачи поиска div и mod:
<(x ≥ 0) ^ (y >0)> S <(x = q * y + r) ^ (0 ≤ r < y)>
Соотношение (1) определяет частичную корректность программы,
так как S может не завершаться, точка выхода может не
достигаться. Завершаемость S необходимо доказать, тогда
будет доказана полная корректность.

10. Спецификация программы и правила вывода

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

11.

Представим блок-схему этого алгоритма как композицию…..
x>=0, y>0
x>=0, y> 0
s1
q = 0;
r>=0
s1
r = x;
s3
x=q*y+r, 0 x=q*y+r, r>=0

12.

x = q*y + r, r >=y
r = r – y;
S3
s2
q = q + 1;
x = q * y +r , r >=O

13. Правила вывода

Правила вывода – это схемы рассуждений, позволяющие
доказывать свойства программ. Общий вид:
H1,H2,…Hn
H
Если над чертой истинные выражения, то и под чертой выражение
будет истинным.
Первое правило консеквенции:
S , R
Q
S
Например:
<(x >0) ^ (y > 0)> S <(z + u * y = x * y) ^ (u = 0)>,
(z + u * y = x * y) ^ (u = 0)
(z = x * y)
<(x >0) ^ (y > 0)> S <(z = x * y)>

14. Второе правило консеквенции:

15. Правила вывода для операторов языка программирования

16. Правила вывода для структурных операторов

Простейшей формой структурирования является создание
составных операторов с помощью последовательной
композиции действий S1, S2,… Sn.
В С++ составной оператор —

17. Правила вывода для составного и условных операторов

18. Правила вывода для условных операторов

Если мы хотим доказать истинность утверждения
if (B) S1; else S2
то необходимо доказать истинность двух утверждений.
1. Так как P справедливо перед выполнением оператора if и, если
выполняется оператор S1, то перед выполнением оператора if
должно быть истинно условие B, а это значит, что должно быть
истинно и выражение P^B. Но если после выполнения оператора if
выполняется условие Q, то первое утверждение, которое должно
выполняться, запишется в виде:
S1

19. Правила вывода для условных операторов

2. Если B ложно, то будет выполняться оператор S2. Так как P было
истинно перед выполнением if, делаем вывод, что перед
выполнением S2 справедливо соотношение P ^ ¬B. И так как
после выполнения S2 должно выполняться Q, то второе
утверждение запишется так: S2

20. Правила вывода для условных операторов

Сокращенный условный оператор:
if ( B ) S;
Блок-схема сокращенного условного оператора:
P
B
P^B
S
Q
1. S

21. Правила вывода для условных операторов

22. Итерационная композиция, операторы циклов

Оператор цикла с предусловием:
while (B) S;
B – выражение, S – оператор, простой или составной.
S выполняется пока условие B выполняется, имеет истинное
значение. Итерационное выполнение S завершается, когда B
становится ложным.

23. Итерационная композиция, операторы циклов

Если P справедливо, когда впервые входим в цикл, то P^B будет справедливо,
если мы достигнем точки C. Если же придем в точку D, т.е. цикл завершится
нормально, то должно выполняться условие P^ ¬ B. Но после выполнения
оператора S, мы снова попадем в точку А и снова должно выполняться
условие P. Т.е. в точке A условие P, а в точке С условие P^B , будут
выполняться столько раз, сколько раз выполняется тело цикла.
S
< P >while (B) S; < P ^ ¬ B >
Говорят, что это правило устанавливает свойство инвариантности
утверждения P, поэтому P называют инвариантом цикла.

24. Правило вывода для цикла с постусловием: do S while B;

A –P
S
Q ^ B —
C —Q
B
Истина
Ложь
D —Q ^ ¬ B
P будет истинно всякий раз, когда достигается точка A, и Q будет
истинно в точке С независимо от числа повторений цикла. Когда
достигается точка D, должно быть истинно утверждение Q ^ ¬ B.

25. Правило вывода для цикла с постусловием: < P >S < Q >, Q ^ B P < p >do S while (B);

Пример.
Доказательство правильности алгоритма поиска div и mod
Представим блок-схему этого алгоритма с учетом его декомпозиции
— x>=0, y>0
—x>=0, y> 0
s1
q = 0;
— x=q*y+r, r>=0
s1
r = x;
s3
— x=q*y+r, 0 — x=q*y+r, r>=0

26. Доказательство правильности алгоритма поиска div и mod

S3
s2
x=q*y + r, r>=y
r = r – y;
q = q + 1;
x = q * y +r , r>=O

27. Фрагмент программы

28. Рассмотрим вначале цикл, представленный блоком s3 B — это (r >= y) , отрицание B – это ( r < y ) Переписав выходное соотношение

Рассмотрим вначале цикл, представленный блоком s3
B — это (r >= y) , отрицание B – это ( r < y )
Переписав выходное соотношение с использованием этих
выражений, получим:
Т.е. необходимо доказать, корректность цикла

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

где s2 – составной оператор, отраженный блок-схемой. Докажем
это соотношение. Для этого используем утверждение, которое
следует из того, что если из r вычесть y, то к q необх. прибавить 1.
Используем дважды правило вывода для оператора присваивания

30. Теперь используем правило составного оператора и 2-е правило консеквенции

31.

Это и есть выражение над чертой в нашем случае S2 , т. обр. правило вывода для цикла s3 доказано.
Использовав эти три соотношения и правило консеквенции,
получим соотношение для s1.
<(x>=0) (y>0)> s1 <(x = q*y + r) (r>=0)>
32. Осталось доказать спецификацию для составного оператора

33.

Элементы доказательного программирования

Доказательное программирование — это составление программ с доказательством их правильности. Сложность составления и доказа­тельства правильности алгоритмов и программ состоит в следующем.

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

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

Существуют два подхода к проверке программ — прагматический и доказательный. При прагматическом подходе проверка программ выполняется на ЭВМ путем тестирования.

Тестирование — это проверка программ на ЭВМ с помощью не­которого набора тестов. Ясно, что тестирование не дает гарантий правильности выполнения программ на всех допустимых данных. Следовательно, тестирование в общем случае не может дать и не дает полных гарантий отсутствия ошибок в программах.

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

По этой же причине не ясно, когда процесс отладки программ — процесс поиска и исправления ошибок на ЭВМ — может считаться завершенным. А выявлены или нет все ошибки в программе при ее отладке не может сказать никто.

Таким образом, прагматический подход чреват созданием про­грамм, содержащих ошибки даже после «завершения» отладки, что и наблюдается практически во всех больших программах для ЭВМ.

Рассмотрим в качестве иллюстрации принципов тестирования алгоритм и программу вычисления максимума из трех чисел: а, b, с.

алг «максимум трех чисел» ‘максимум трех чисел

нач cls

ввод (а, b, с) input a, b, с

если а > b то if а > b then

тах:= a max = a

инеc b > с то elseif b > с then

тах:= b mах = b

инеc с > а то elseif с > a then

тах:= с mах = с

кесли end if

вывод («тах=»,тах)? «mах=»; mах

кон end

Запуск этой программы на ЭВМ можно проверить на следующих данных:

? 1 1 2? 1 2 3? 3 2 1

max = 2 max = 3 max = 3

Все три результата правильные. Отладку программы после запуска этих примеров можно было бы считать завершенной. Однако есть контрпример:

Контрпример1

Но этот результат — неправильный. Следовательно, алгоритм и программа содержат ошибки. Но сколько этих ошибок — одна, две, а может быть больше?

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

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

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

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

алг «у = х 5 » Результаты Утверждения

Нач

v:= х×х v1 = х×х Þ v1 = x 2

у:= v×x у = v2×x Þ у = х 5

Кон

Справа от алгоритма приведены результаты выполнения присва­иваний. Результатом первого присваивания v:= х×х будет значение v1 = х×х переменной v. Результат следующего присваивания v:= v×v — второе значение переменной v, равное v2 = v1×v1. Результатом треть­его присваивания у:= v×x будет значение у = v2×x.

На основе приведенных рассуждений, можно сделать три утверж­дения о промежуточных и конечных результатах вычислений:

Таким образом можно высказать окончательное

Утверждение. Конечным результатом выполнения будет

у = х 5 для любых значений х.

Доказательство. Исходя из описания результатов выполнения присваиваний значение у будет равно

Что и требовалось доказать.

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

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

алг «у = тах(а, b,с)» Результаты

Нач

если а > b то при а > b

у:= а у = а

инес b > с то при b > с

у:= b у = b

инес с > а то при с > а

у:= с у = с

кесли при не (b > с)

Кон

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

у = b, при b > с и b ³ а,

с, при с > а и с ³ b.

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

а, при а ³ b и а ³ с,

mах = b, при b ³ с и b ³ а,

с, при с ³ а и с ³ b.

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

Для опровержения общего утверждения достаточно указать хотя бы один контрпример. В данном случае утверждение о правильности алгоритма гласило бы: для любых значений переменных а, b, с конечным было бы значение mах (а, b, с).

Контрпримером в данном случае будут значения: а = 2, b = 1, с = 3. Для этих данных по определению mах = 3, а по результатам выполнения алгоритма у = 2. Следовательно, в алгоритме содержится ошибка.

Однако оказывается, что это не единственная ошибка. Более тон­кие ошибки вскрывает второй контрпример: а = 1, b = 1, c = 1. Для этих данных в алгоритме вовсе не определен результат вычислений у =? и конечный результат выполнения программы будет непред­сказуем!?

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

Постановка задачиМетод решения

Вычисление mах (а, b, с).

Дано: а, b, с — три числа, mх = mах(mах(а,b),с)

Треб.: mх — максимум, mах(х,у) = х, при х ³ у

Где: mх = mах (а, b, с). у, при у ³ х