Программная реализация

Программная реализация решения задачи выполнена на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