Теоретическое исследование моделей программы, решающей заданную задачу
Дипломная работа - Компьютеры, программирование
Другие дипломы по предмету Компьютеры, программирование
ия
Константы:
I(a)=0;
Функции(f)=F, F(x)=x+1;
Предикаты(p1)=P1, P1(i,x)=true, еслиiy;
Протокол выполнения
На вход подан массив угловых коэффициентов уравнений a= {1,2,2}
СостояниеМеткаПеременные anumijall_per 1{1,2,2}3UUU 2{1,2,2}3UU0 3{1,2,2}30U0 4{1,2,2}30U0 5{1,2,2}3010 6{1,2,2}3010 7{1,2,2}3010 8{1,2,2}3011 9{1,2,2}3021 6{1,2,2}3021 7{1,2,2}3021 8{1,2,2}3022 9{1,2,2}3032 6{1,2,2}3032 10{1,2,2}3132 4{1,2,2}3132 5{1,2,2}3122 6{1,2,2}3122 7{1,2,2}3122 9{1,2,2}3132 6{1,2,2}3132 10{1,2,2}3232 4{1,2,2}3232 11{1,2,2}3232
Инварианты и ограничения циклов
Внешний цикл по i
Предусловие Q:i < num - 1
Постусловие R: i=num - 1
Ограничивающая функция t: num -1- i
ИнвариантP:0? i? num-1
Внутренний цикл по j
Предусловие Q:j<num
Постусловие R:j = num
Ограничивающая функция t:num - j
Инвариант P: 1?j? num
Доказательство частичной и полной правильности программы
Доказательство частичной правильности подразумевает доказательство того, что цикл перебирает все пары. А полное, подразумевает, что после получения ответа программа завершится.
Для доказательства частичной правильности необходимо показать, что цикл переберёт все пары. Это можно сделать с помощью метода индуктивных утверждений.
При первом попадании в точку Т1 i=0. Утверждение 0 ? i? num-1верно.
Предположим, что в результате выполнения программы было попадание в точку Т1 с i=n. Докажем, что будет попадание в точку Т1 с i=n+1.
В точке Т1 при i=t отношение 0 ? i? num-1истинно, так как n<numи n?0. Следовательно, цикл выполнится ещё раз, c увеличится на 1, произойдёт попадание в точку Т1 с i=n+1.
Для доказательства полной правильности необходимо показать, что цикл когда-нибудь завершится. Так как на каждой итерации iувеличивается на 1, а величина num-1 не изменяется, то когда-нибудь значение cстанет равно n, следовательно, выражение i<num-1 перестанет выполняться, и цикл завершится.
Таким образом, доказана частичная и полная правильность основного цикла программы. На основании этого можно сделать вывод, что программа решает поставленную задачу правильно.
Схема программы в виде сети Петри
a: read(a[],num);: all_per=0;: i=0;: i< num-1;: j=i+1;: g<num;: a[i]==a[j];: all_per=all_per+1;
i: j=j+1;: i=i+1;
Рисунок 2
Дерево достижимости
Рисунок 3
Анализ свойств сетей Петри на основе дерева достижимости
Анализ безопасности и ограниченности.
Сеть Петри ограниченна тогда и только тогда, когда символ w отсутствует в ее дереве достижимости. Отсутствие символа wв дереве достижимости означает, что множество достижимых маркировок конечно. Следовательно, простым перебором можно найти верхнюю границу, как для каждой позиции в отдельности, так и общую верхнюю границу для всех позиций. Последнее означает ограниченность сети Петри. Полученная сеть Петри безопасна, потому что граница для всех позиций равна 1.
Анализ сохранения.
Так как дерево достижимости конечно, для каждой маркировки можно вычислить сумму начальной маркировки. Сеть Петри является сохраняющей, так как для каждой маркировки сумма начальной маркировки равна 1. Она одинакова для каждой достижимой маркировки.
Анализ покрываемости.
В данной сети Петри ни одна маркировка m' не является покрываемой, так как среди вершин дерева достижимости не существует такой вершины x, что m[x]m'.
Анализ живости.
Переход t сети Петри является потенциально живым, тогда и только тогда, когда он метит некоторую дугу в дереве достижимости этой сети. Все переходы t сети Петри являются потенциально живыми, т.к. существует такая R(N, ), что t разрешен в .
Вывод
В результате выполнения курсовой работы была написана программа, решающая поставленную задачу, а именно, подiет количества пересечений прямых, заданных двумя точками. Была представленная стандартная схема программы, решающей заданную задачу. Алгоритм вычислений был охарактеризован приведенной интерпретацией. Был составлен протокол выполнения программы в виде последовательности конфигураций. Из которого видно, каким образом изменяются переменные в ходе работы программы и какие значения получаются в результате. Доказательства частичной и полной правильности программ позволяют сделать вывод, что программа не зациклится и за конечное время будет получен результат. Была построена сеть Петри, и на основе дерева были исследованы ее свойства: построенная сеть Петри является потенциально живой, ограниченной, безопасной, и сохраняющей.
Таким образом, результат данных исследований позволяет сделать вывод о правильности программы.
Список используемой литературы
1. Рабинович Е.В. Теория вычислительных процессов, учебное пособие - Новосибирск, 2004.
. Котов В.Е. Сети Петри - М.: Наука, 1984.