Лабораторная работа 6 ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ ПРОГРАММ МЕТОДОМ ПРОГРАММНЫХ ФУНКЦИЙ Цель работы- ов
Работа добавлена на сайт samzan.net:
Лабораторная работа 6
ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ ПРОГРАММ МЕТОДОМ ПРОГРАММНЫХ ФУНКЦИЙ
Цель работы: овладение техникой доказательства правильности линей ных, ветвящихся и циклических структурированных прог рамм.
Контрольные вопросы
1. Какова стратегия доказательства правильности не элементар ных структурированных программ?
2. Назначение аксиомы замещения?
3. Как формулируется лемма о сведении циклических программ к рекурсивным?
4. Методика доказательства правильности циклических программ?
5. Назначение и структура трассировочных таблиц?
Методические указания
Если программа Р не является элементарной программой, то при доказательстве правильности пароизводится разложение Р на элемен тарные составляющие программы. Пусть, например, имеется функция f и соответствующая программа F = IF p THEN G ELSE H FI, где G и H являются также программами. Вместо прямой верификации равенства
f = [IF p THEN G ELSE H FI] доказательство правильности проводится
в два этапа:
- в первую очередь доказывается правильность составляющих программ G и H на основе предположения об их программных функциях g и h, т.е. доказывается, что g=[G] и h=[H];
- если первый этап доказательства завершился успешно, то про водится доказательство равенства f=[IF p THEN g ELSE h FI].
Правомочность подстановки в программу F вместо программ G и H их программных функций g и h базируется на аксиоме замещения [ ].
Если верифицируемая программа Р является ациклической, то до казательство правильности может быть проведено непосредственным построением [P] по схеме выполнения программы и сравнением [P] с заданной функцией f.
Верификацию циклических программ типа WHILE-DO, DO-UNTIL, DO WHILE-DO можно свести к доказательству их окончания и к доказа тельству правильности ациклических рекурсивных программ. Сведение циклических программ к рекурсивным основано на следующей лемме [ ].
Лемма. Пусть даны функции f, g, h и предикат p. Тогда:
а) (f=[WHILE p DO g OD]) <--> (fin(f, WHILE p DO g OD) & f=[IF p THEN g; f FI]);
б) (f=[DO g UNTIL p OD]) <--> (fin(f, DO g UNTIL p OD) & f=[g; IF - p THEN f FI]);
в) (f=[DO1 g WHILE p DO2 h OD]) <--> (fin(f, DO1 g WHILE p DO2 h OD) & f=[g; IF p THEN h; f FI]).
где fin(f,P) - предикат, принимающий значение "истина" когда программа Р заканчивается для любого Х из области определения функции f.
Для вывода программных функций можно использовать трассиро вочные таблицы [ ].
Пример 1. Необходимо построить программную функцию для прог раммы
x := x + a;
y := y + x;
x := x - y;
Трассировочная таблица для этой программы будет иметь вид:
|
Шаг |
Оператор программы |
Д а н н ы е |
|||
|
X |
Y |
||||
|
1 2 3 |
x := x+a y := y+x x := x-y |
x1:= x2:= x3:= |
x0 + a x1 x2 – y2 |
y1:= y2:= y3:= |
y0 y1 + x1 y2 |
Все данные в таблице имеют индексы, соответствующие шагам вычислений, индекс начальных значений данных равен нулю. Из трассировочной таблицы легко вывести функцию программы:
x3 : = x2 – y2 := x1 – y1 – x1 := -y1 = -y0
y3 : = y2 := y1 + x1 := y0 + x0 + a
Следовательно, приведенная программа имеет функцию
x , y := -y , y+x+a.
Задание к лабораторной работе
Методом программных функций доказать правильность программы, выполняющей заданную обработку массива (см. табл.). Составить структурированную программу (блок-схему) и выполнить ее верификацию с использованием программных функций.
Порядок выполнения работы
При верификации структурированной программы на основе прог раммных функций следует придерживаться следующей методики:
- составить структурированную программу обработки массива;
- с помощью декомпозиции разбить исходную программу на ряд более простых программ и доказать правильность каждой из них в от дельности;
- используя аксиому замещения, доказать правильность исход ной программы.
Если какая-нибудь подпрограмма является ациклической, то до казательство правильности проводится на основе построения её Е-схемы.
В случае циклической программы методика верификации состоит в следующем:
- формулируется гипотеза о программной функции (она может быть и задана);
- путем анализа программы устанавливается истинность условия окончания fin(f,p);
- с использованием леммы о рекурсивном представлении цикли ческая подпрограмма приводится к рекурсивной форме;
- с помощью трассировочных таблиц строится программная функ ция рекурсивной подпрограммы;
- проводится сравнение полученной функции с гипотезой и де лается вывод о правильности программы.
Содержание отчета
1. Название и цель работы.
2. Блок-схема верифицируемой программы.
3. Доказательство правильности программы методом программных функций.
Таблица 1
|
N варианта |
Задание по обработке массива чисел |
|
1 |
2 |
|
1. 2. 3. 4. 5. 6. 7. 8. 9. 10. 11. 12. 13. 14. 15. 16. 17. 18. |
Упорядочение элементов по возрастанию Определение минимума Нахождение суммы элементов Замещение отрицательных элементов массива нулями Упорядочение элементов по убыванию Определение максимального элемента Определение места заданного элемента в массиве Определение суммы отрицательных элементов Упорядочение по возрастанию абсолютных величин Определение суммы квадратов Подсчет количества положительных элементов Подсчет количества отрицательных элементов Упорядочение по убыванию абсолютных величин Определение произведения элементов Подсчет количества одинаковых элементов заданной величины Определение среднего арифметического Определение минимального положительного элемента Определение максимального отрицательного элемента |
|
19. 20. 21. 22. 23. 24. 25. 26. 27. 28. |
Определение максимального положительного элемента Определение минимального отрицательного элемента Определение суммы положительных элементов Определение произведения положительных элементов Нахождение суммы модулей Определение суммы четных элементов Определение произведения отрицательных элементов Выделение первых K положительных элементов Пересылка положительных элементов в начало Нахождение среднего геометрического |
2. РИНХ Факультет коммерции и маркетинга Рассмотрено и
3. Понятие природноресурсного потенциала
4. 24498
5. 13 h z u ВВЕДЕНИЕ
6. PROBBILITY Wht is the probbility tht the chosen letter is
7. задание компьютерной практики фрагмент отсканированного текста
8. Полесский государственный университе
9. Тема 1 Міжнародна економічна система Сутність та структура міжнародної економічної системи
10. тема правовых норм регулирующих имущественные а также связанные и некоторые не связанные с ними личные неим
11. Реферат- Процесс развития личности
12. лекция Отличие искусства от религии и философии
13. Идея 630063 г Новосибирск ул
14. Условие для C T не выполнено или Условие для DT не выполнено
15. Дифференциальное уравнение теплопроводимости
16. Анализ платежеспособности и финансовой устойчивости Енотаевского райпотребсоюза
17. САНКТПЕТЕРБУРГСКИЙ ИНСТИТУТ ВНЕШНЕЭКОНОМИЧЕСКИХ СВЯЗЕЙ ЭКОНОМИКИ И ПРАВА Филиал в г
18. Определить скорости и ускорения во всех узлах механизма
19. а В этот период создается теоретическая программа реализма
20. Экологическое прав