архитектура / Лабор. работа 5 по Архит_и_проект ПО

Лабораторная работа 5

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

Цель работы: овладение техникой доказательства правильности линейных, ветвящихся и циклических структурированных программ.

Контрольные вопросы

1. Какова стратегия доказательства правильности не элементар­ных структурированных программ?

2. Назначение аксиомы замещения?

3. Как формулируется лемма о сведении циклических программ к рекурсивным?

4. Методика доказательства правильности циклических программ?

5. Назначение и структура трассировочных таблиц?

1. Методические указания

Если программа Р не является элементарной программой, то при доказательстве правильности производится разложение Р на элемен­тарные составляющие программы. Пусть, например, имеется функция 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 базируется на аксиоме замещения [5].

Если верифицируемая программа Р является ациклической, то до­казательство правильности может быть проведено непосредственным построением [P] по схеме выполнения программы и сравнением [P] с заданной функцией f.

Верификацию циклических программ типа WHILE-DO, DO-UNTIL, DO­WHILE-DO можно свести к доказательству их окончания и к доказа­тельству правильности ациклических рекурсивных программ. Сведение циклических программ к рекурсивным основано на следующей лемме [5, 9, 10].

Лемма. Пусть даны функции 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.

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

Пример 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

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

x₃ : = x₂ – y₂ := x₁ – y₁ – x₁ := -y₁ = -y₀

y₃ : = y₂ := y₁ + x₁ := y₀ + x₀ + a

Следовательно, приведенная программа имеет функцию

x , y := -y , y+x+a.

Пример 2. Верифицировать программу для вычисления произведения элементов массива чисел.

2. Задание к лабораторной работе

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

Таблица 1

№ варианта	Задание по обработке массива чисел
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	Определение минимума Нахождение суммы элементов Замещение отрицательных элементов массива нулями Определение максимального элемента Определение места заданного элемента в массиве Определение суммы отрицательных элементов Определение суммы квадратов Подсчет количества положительных элементов Подсчет количества отрицательных элементов Определение произведения элементов Подсчет количества одинаковых элементов заданной величины Определение среднего арифметического Определение минимального положительного элемента Определение максимального отрицательного элемента Определение минимального отрицательного элемента Определение суммы положительных элементов Определение произведения положительных элементов Нахождение суммы модулей Определение суммы четных элементов Определение произведения отрицательных элементов Выделение первых K положительных элементов Пересылка положительных элементов в начало Нахождение среднего геометрического Определение максимального положительного элемента

3. Порядок выполнения работы

При верификации структурированной программы на основе прог­раммных функций следует придерживаться следующей методики:

- составить структурированную программу обработки массива;

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

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

Если какая-нибудь подпрограмма является ациклической, то до­казательство правильности проводится на основе построения её Е-схемы.

В случае циклической программы методика верификации состоит в следующем:

- формулируется гипотеза о программной функции (она может быть и задана);

- путем анализа программы устанавливается истинность условия окончания fin(f,p);

- с использованием леммы о рекурсивном представлении цикли­ческая подпрограмма приводится к рекурсивной форме;

- с помощью трассировочных таблиц строится программная функ­ция рекурсивной подпрограммы;

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

4. Содержание отчета

1. Название и цель работы.

2. Блок-схема верифицируемой программы.

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