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

Вопросы

1. К чему приводят ошибки в экономических программах?

2. Кто отвечает за ошибки в экономических программах?

3. Что дают постановки задач?

4. Зачем нужны описания методов?

5. Как проверяется правильность методов?

6. Зачем нужны описания результатов?

Задания

1. В магазине имеются товары различных наименований. В течение дня каждый из М покупателей (М - заданное число) сообщил о своем намерении приобрести определенное количество товара одного из на­именований. Требуется определить суммарный спрос на товары каждого наименования, расположив товары в порядке убывания дневного спроса на них.

2. Каждый из N магазинов в течение месяца работал D дней (N и D - заданные числа 1, 2,.... N). Известна прибыль каждого магазина в каждый день его работы. Необходимо напечатать упорядоченный по месячным доходам список названий магазинов, имеющих прибыль в пересчете на один день работы выше средней дневной прибыли по всем магазинам.

3. Каждое из N предприятий города выпускает М одинаковых на­именований продукции (N и М, наименования продукции и названия предприятий известны). Заданы объем выпуска и стоимость единицы продукции каждого вида для каждого из предприятий. Необходимо для каждого вида продукции определить предприятия, выпускающие наибольший объем этой продукции.

4. Из разных городов выбрали N семей (N - заданное число). Каждая семья характеризуется числом членов и доходом каждого изних.Для каждого города сформировать перечень семей с минимальным доходом в пересчете на отдельного члена семьи, указав порядковые номера семей из общего списка.

5. Ассортимент N магазинов состоит из М товаров (N, М и названия товаров заданы). Каждый товар характеризуется наличием или отсутст­вием его в магазине, а также наличием или отсутствием на него спроса покупателей. Требуется перечислить названия ходовых (есть спрос и товар имеется хотя бы в одном магазине), неходовых (спрос отсутствует, а товар имеется хотя бы в одном магазине) и дефицитных (спрос есть, а товара нет ни в одном из магазинов) товаров.

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

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

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

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

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

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

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

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

Рассмотрим в качестве иллюстрации принципов тестирования алгоритм и программу вычисления максимума из трех чисел: а, 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

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

Tecт₁ Тест₂ Тест₃

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

max = 2 max = 3 max = 3

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

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

? 2 1 3

max = 2

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

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

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

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

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

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

Дата добавления: 2014-11-25