Программная реализация
Программная реализация решения задачи выполнена наC# в VisualStudio 2008.calc() // нахождение количества точек пересечия {i, j;_per = 0;(i = 0; i < num - 1; i++)(j = i + 1; j < num; j++) {(b_arr[i] != b_arr[j]) all_per++; } }
Результаты проведённого исследования ССП в графовой форме
Рисунок 1 ССП в линейной форме 1: start(a[],num) goto 2 2: all_per:=a goto 3 : i:=b goto 4 : if p1(i,num) then goto 5 else goto 11 : j:=f(i)i goto 6 : if p2(j,num) then goto 7 else goto 10 : if p3(a[i],a[j]) then goto 8 else goto 9 : all_per:=f(all_per) goto 9 : j:=f(j) goto 6 : i:=f(i) goto 4 11: stop (all_per) Интерпретация Константы: I(a)=0; Функции(f)=F, F(x)=x+1; Предикаты(p1)=P1, P1(i,x)=true, еслиi<x-1;(p2)=P2, P2(j,x)=true, еслиj<x;(p3)=P3, P3(x,y)=true, еслиx<>y;
Протокол выполнения
На вход подан массив угловых коэффициентов уравнений a= {1,2,2}
Инварианты и ограничения циклов
Внешний цикл по 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
Популярное: Как построить свою речь (словесное оформление):
При подготовке публичного выступления перед оратором возникает вопрос, как лучше словесно оформить свою... Как распознать напряжение: Говоря о мышечном напряжении, мы в первую очередь имеем в виду мускулы, прикрепленные к костям ... Модели организации как закрытой, открытой, частично открытой системы: Закрытая система имеет жесткие фиксированные границы, ее действия относительно независимы... ©2015-2024 megaobuchalka.ru Все материалы представленные на сайте исключительно с целью ознакомления читателями и не преследуют коммерческих целей или нарушение авторских прав. (160)
|
Почему 1285321 студент выбрали МегаОбучалку... Система поиска информации Мобильная версия сайта Удобная навигация Нет шокирующей рекламы |