МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ
ФЕДЕРАЛЬНОЕ АГЕНТСТВО ПО ОБРАЗОВАНИЮ
ГОСУДАРСТВЕННОЕ ОБРАЗОВАТЕЛЬНОЕ УЧРЕЖДЕНИЕ ВЫСШЕГО
ПРОФЕССИОНАЛЬНОГО ОБРАЗОВАНИЯ
НОВОСИБИРСКИЙ ГОСУДАРСТВЕННЫЙ ТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ
ФАКУЛЬТЕТ АВТОМАТИКИ И ВЫЧИСЛИТЕЛЬНОЙ ТЕХНИКИ
КАФЕДРА АВТОМАТИКИ
Расчётно-графическое задание (Часть 1)
по дисциплине «Теория вычислительных процессов»
на тему:
«Доказательство правильности методом индуктивных утверждений»
Факультет: АВТ Преподаватель:
Группа: АВТ-918
Вариант: 7
Выполнил:
Новосибирск, 2013
Задание:
1. Для данной задачи составить блок-схему и доказать ее правильность методом индуктивных утверждений.
2. Для данной задачи написать программу на языке высокого уровня и доказать ее правильность. Доказательство проводить методом индуктивных утверждений, включая индуктивные утверждения в текст программы в виде комментариев.
Постановка задачи:
Для матрицы ANxM найти сумму наименьших элементов строк.
Решение:
1.
Рис.1.Блок-схема алгоритма.
Прежде чем доказывать правильность, нам необходимо убедиться, что алгоритм конечен.
В ходе программы значения N и M не меняются, а изменяются только значения I и J. Т. к. с каждым шагом цикла I и J увеличиваются на 1, то рано или поздно они достигнут значений I=N, J=M.
Рассмотрим внутренний цикл. Т. к. значение M не меняется внутри цикла, J через конечное число итераций достигнет значения M. При попадании в точку 4 после конечного числа шагов мы попадаем в точку 8 и затем – в точку 3. Это случится, когда J будет не меньше, чем M. При этом I увеличится на 1 и через конечное число шагов так же достигнет значения N, которое не меняется ни внутри внешнего, ни внутри вложенного цикла.
Когда I будет не меньше, чем N, произойдет прерывание цикла и переход из точки 3 в точку 9, что и будет являться завершением алгоритма.
Теперь необходимо доказать правильность блок-схемы методом индуктивных утверждений.
1 → 2 → 3.
Предположим, что данные, связанные с точкой 1, удовлетворяют исходному допущению. При попадании из точки 1 в точку 3 мы имеем summ=0 и I=0. Очевидно, что I входит в промежуток [0;N] и summ=0. Утверждение о summ так же справедливо.
3 → 4.
Если мы находимся в точке 3 и соответствующее утверждение верно, и из этой точки мы переходим в точку 4, то утверждение 4 тоже будет справедливо. На пути выполняются только присваивания min = Ai0 и J=0. Т. к. массив неизменен, то утверждение, касающееся массива, остается справедливым в точке 4. Если учесть, что mini=Ai0, то справедливо утверждение mini≤Aij, т. е. mini≤Аi0 на данном шаге. Поскольку J=0 и 0≤J≤M, то утверждение в точке справедливо.
4 → 5 → 7 → 4.
Мы находимся в точке 4, и соответствующее утверждение справедливо. Пройдя через точки 5 и 7, мы вернемся в исходную точку 4, утверждение в которой должно остаться справедливым.
Переход по данному пути возможен только при невыполнении условия Аij<min. При этом переменная принимает новое значение Jm+1, которое соответствует Jm+1. Поскольку на данном пути происходит лишь присваивание (при неизменном M, min и массиве А) и 0≤Jm+1≤M, утверждение справедливо.
4 → 5 → 6 → 4.
В данном случае проверка Аij<min должна оказаться истинной. При этом по возвращении в точку 4, соответствующее утверждение должно оказаться справедливым.
На данном пути две переменные меняют свое значение. Таким образом, minm+1= Аij и Jm+1= Jm+1. При этом происходит только присваивание при неизменных А и M. В точке 4 продолжает выполняться условие 0≤Jm+1≤M и minm+1= Аi(m+1), утверждение справедливо.
4 → 8 → 3 .
Допустим, утверждение J<M было ложным, и мы движемся по пути от точки 4 к точке 8. Раз так, то очевидно, что Jm=M, учитывая, что 0≤J≤M.
Тогда переменная на (n+1)-м шаге внешнего цикла minn+1 является минимальным из всех элементов массива А. Т. е. minn+1≤A(n+1)0≤A(n+1)1≤…≤A(n+1)(M-1). При этом происходит два присваивания.
Значение summ представляет собой сумму всех минимальных элементов, найденных ранее.
Таким образом, summn+1= summn+minn+1=min0+min1+…+minn+1, что удовлетворяет утверждению в точке 3.
Сама же переменная In+1=In+1, что в свою очередь удовлетворяет
0≤ In+1≤N.
Утверждения, связанные с точками 8 и 3 и касающиеся summ и I – справедливы.
3 → 9.
Если мы проходим по этому пути, то, следовательно, проверка I<N была ложной. В таком случае In=N. Утверждение, касающееся summ в точке 3 при I=N совпадает с утверждением в точке 9.
Таким образом, если объединить это доказательство с предыдущим доказательством конечности программы, то отсюда следует полная правильность программы.
2.
#include <stdio. h>
#include <iostream>
float MinimalElem(float *);
float Summ(float **);
int N=4, M=4;
float MinimalElem(float *line)
{
float min;
min=line[0];
for (int j=0; j<M; j++) //ТОЧКА (3) , ТОЧКА (7) - выход
{
//поиск минимального элемента в строке
//0<= j <= M;
//min=line[j] or min<line[j]
if (min>line[j]) min=line[j]; //ТОЧКА (4) – T, ТОЧКА (5) - F
}
return min;
}
float Summ(float **A)
{
//ТОЧКА (1)
float summ=0;
for (int i=0; i<N; i++) //ТОЧКА (2) , ТОЧКА (8) – STOP summ= MinimalElem(A[0])+…+ MinimalElem(A[N]);
//прибавление к минимальному э-ту (i-1)-ой строки минимального элемента i-ой строки
//summ = MinimalElem(A[0]) + MinimalElem(A[1]) +…+ MinimalElem(A[i])…
//0<= I <= N
summ+=MinimalElem(A[i]); //ТОЧКА (6)
return summ;
}
void main ()
{
float B[4][4] = {{1.0, 2.1, 4.0, 11.3},
{1.5, 13.2, 7.8, 1.3},
{5.0, 16.45, 6.6, 2.12},
{7.8, 5.0, 4.0, 13.2}};
float **A;
A = new float*[N];
for (int i=0;i<N ;i++)
{
A[i] = new float[M];
for (int j=0; j<M; j++)
A[i][j]=B[i][j]; //инициализация двумерного массива A[N][M]
}
printf("\n Summ = %f", Summ(A));
system("pause");
};
Рассмотрим работу программы на примере заданной матрицы 4х4. Для удобства было добавлено две функции, MinimalElem для реализации внутреннего цикла алгоритма, и Summ – для реализации внешнего.
Для начала необходимо доказать конечность программы.
Разберем первый цикл функции MinimalElem:
min=line[0];
for (int j=0; j<M; j++)
{
if (min>line[j]) min=line[j];
}
return min;
На входе в цикл переменная j принимает значение 0. При этом на каждом шаге значение будет увеличиваться на 1 до тех пор, пока не будет выполнено условие выхода из цикла j=M.
Рассмотрим внешний цикл:
float summ=0;
for (int i=0; i<N; i++)
summ+=MinimalElem(A[i],M);
return summ;
Каждый раз при выходе из внутреннего цикла, во внешнем цикле переменная i увеличивается на 1. Совершенно очевидно, что цикл конечен, т. к. за конечное число шагов переменная i с нуля увеличится до N, что будет означать завершение цикла.
Теперь можно доказать правильность программы.
1 → 2.
Поскольку очевидно, что summ=0 и 0<=i<=N, утверждение в точке 2 справедливо.
2 → 3.
min = line[0], что позволяет сделать вывод, что утверждение min<=line[j] – справедливо. Так же справедливо и j=0, т. к. 0<=j<=M
3 → 4 → 3.
В случае, если проверка пройдена и min > line[j], то min = line[j], что в свою очередь говорит, что утверждение min=line[j] справедливо. Так же значение j не превышает N.
3 → 5 → 3.
В том случае, если проверка не пройдена, min < line[j], что в свою очередь говорит, что утверждение min<line[j] справедливо. Так же значение j не превышает N.
3 → 7 → 6 → 2.
В случае, когда проверка j<М дает ложь, переходим к точке 7, затем через 6 ко 2. Очевидно, что j=M и утверждение 0<=j<=M справедливо.
При этом на 6ой точке summ+=MinimalElem(A[i]), т. е. к значеню суммы на предыдущем шаге прибавляем минимальный элемент с текущего шага, что соответствует утверждению summ = MinimalElem(A[0]) + MinimalElem(A[1]) + MinimalElem(A[2])… .
По окончании вложенного цикла переменная i увеличивается на 1, при этом утверждение 0<=i<=N остается справедливым.
2 → 8.
В случае, когда проверка j<М дает ложь, переходим к точке 8 из 2. При этом summ += MinimalElem(A[j]) соответствует записи summ= MinimalElem(A[0])+…+ MinimalElem(A[N]). Таким образом, утверждение справедливо. Так же справедливо и то, что 0<=i<=N, т. к. i=N.
