Теоретическое исследование моделей программы, решающей заданную задачу

Курсовой проект - Компьютеры, программирование

Другие курсовые по предмету Компьютеры, программирование

, эквивалентности. Решение этих задач ограничено существованием символа w. Символ w означает потерю информации: конкретные количества фишек отбрасываются, учитывается только существование их большого числа.

Линейная схема программы

: begin

: input mas, N

2 : i:=c;

: m:if s(i,a) then goto m1;

: sum1 := a;

:sum2 := a;

: j := k(i);

: l:if s(d,j) then goto l1;

:sum1 : = f(sum1,mas,i,j);

:sum2 := g(sum2,mas,i,j);

: j := inc(j);

: goto l;

:ms :=h(sum1, sum2);

:if m(ms,max) then max := r(ms);

: i := dec(i);

:goto m;

16: output max;

: end.

ССП в графовой форме

Интерпретация

1.Переменные:

mas - массив, содержит матрицу целочисленных элементов.

N - размерность матрицы. Целочисленная переменная.

i, j - счётчики циклов. Целочисленные переменные.

sum1, sum2, ms - переменные для нахождения суммы элементов

max - переменная, содержащая максимальную сумму.

2.Константы:

c = N-1;= 0;= N;

3.Предикаты:

S(x,y) - if x>y => T;

4.Функции:

inc(x) - x++;(x,y) - if x >= y return x; else return y;=3;

Mas = {1, 2, 3,

, 5, 6,

, 8, 9};Протокол

Меткаijsum1sum2msmax12----022- 0--032-00-042000-052070-062073-072173-0921737011217377121173772110377311007741000775104077610427771142775111227761112877712128779121281271112128121212021281212…………………12-1315151515

Инварианты и ограничения циклов

Алгоритм решения задачи::= A[n-1,0];:= -n+1;i 0 j:= 1-i P 1-i 0 j:= 1 fi;i+j m and j n sum:= sum+A[j-1,i+j-1]; j:= j+1 Odmax < sum max:= sum fi:= i+1

Инвариант и ограничивающая функция для внутреннего цикла:

n - количество строк в матрице;

m - количество столбцов в матрице;

P: " j, i: -n+1 i < m and 1 j <n and j m-ij

$ sum: sum = A[k-1, i+k-1] or sum = A[k-1, i+k-1] or sum=0=1 k=1-i

Ограничивающая функция t: m-i-j-1 and n-j

Инвариант и ограничивающая функция для внешнего цикла:

P: " j, i: -n+1 i < m and 1 j <n and j m-ij

$ max: (max A[k-1, i+k-1] or max A[k-1, i+k-1])=1 k=1-ij(max = A[k-1, i+k-1] or max = A[k-1, i+k-1])=1 k=1-i

Ограничивающая функция t: 0-i - для отрицательной части or m-i - для неотрицательной части

Доказательство частичной и полной правильности программы.

Докажем правильность работы внутреннего цикла.

n+1 y <m

r <n+1 and r m-i

" j, i: -n+1 i < m and 1 j <n and j m-ij

$ sum: sum = A[k-1, i+k-1] or sum = A[k-1, i+k-1] or sum=0 (*)=1 k=1-i

При первом попадании в точку Х утверждение (*) выполняется, так как sum=0.
Пусть при p - попадании в точку Х утверждение (*) выполняется. Докажем, что утверждение (*) выполняется при p+1 - попадании в точку Х.

Для p:j

$ sum: sum = A[k-1, i+k-1] or sum = A[k-1, i+k-1] or sum=0=1 k=1-i

Чтобы попасть в точку Х необходимо, чтобы выполнилось условие i+j m and j n и операторы

j j+1= A[k-1, i+k-1] + A[k,i+k] = A[k-1, i+k-1] or=1 k=1j+1= A[k-1, i+k-1] + A[k,i+k] = A[k-1, i+k-1]=1-i k=1-i

Так как условие (i+j m and j n) выполнилось, то i+j+1 m and j+1 n при p+1 - попадании в точку Х утверждение (*) справедливо.

Докажем, что цикл закончится то есть выполнится условие (i+j > m or j > n).

При первом попадании в точку Х: -n+1 i n) и цикл завершится.

Докажем правильность работы внешнего цикла.

" j, r: -n+1 r < i+1 and 1 j <n and j m-rj

$ max: (max A[k-1, r+k-1] or max A[k-1, r+k-1])=1 k=1-rj(max = A[k-1, r+k-1] or max = A[k-1, r+k-1]) (*)=1 k=1-r

При первом попадании в точку Х утверждение (*) выполняется, так как max = A[n-1,0]

j = n, i = 1-n, r = 1-n, k = 1-r = n= A[n-1,1-n+n-1]

n+1 1-n <m and 1 j=n <n+1 and n m-1+n

Пусти при p - попадании в точку Х утверждение (*) выполняется. Докажем, что утверждение (*) выполняется при p+1 - попадании в точку Х.

Для p:

" j, r: -n+1 r < i+1 and 1 j <n and j m-rj

$ max: (max A[k-1, r+k-1] or max A[k-1, r+k-1])=1 k=1-rj(max = A[k-1, r+k-1] or max = A[k-1, r+k-1]) (*)=1 k=1-r

r = -n+p+1.

Чтобы попасть в точку Х необходимо, чтобы выполнилось условие i < m и внутренние вычисления. На выходе внутреннего цикла имеем:

j j

sum = A[k-1, r+k-1] or sum = A[k-1, r+k-1] , где r = -n+p

k=1 k=1-r

Если max, полученный на предыдущих шагах sum, то max остается прежним, вычисленным на предыдущих шагах.

Таким образом, либо r= -n+p, либо r- остается прежним. При обоих вариантах выполняется условие (*).

Докажем, что программа закончится.

Так как в каждым шагом значение i увеличивается, а n и m -конечны и не меняются, то через некоторое время не выполнится условие i < m и цикл завершится.

Анализ сетей Петри на основе дерева достижимости.

Сеть Петри

b.true

c b.false

P12

d.true

Blog

Теоретическое исследование моделей программы, решающей заданную задачу

Курсовой проект - Компьютеры, программирование

Другие курсовые по предмету Компьютеры, программирование