Операции (в программе)

Операции (в программе)

Доказать, что абстрактные выражения эквивалентны конкретным:

Критерий правильности предусловия данных состоит в том, что каждая P_j моделирует соответствующую f_j.

Для доказательства используем функции:

K_T(P(t)) - отображает предикатное условие с абстрактными переменными в его конкретное представление в контексте типа T.

K_НМЦ(h=H) º m=M Ù "k: 0£k<m : b[k]=B[k]

Надо доказать

            - для инициализации {T} Q {K_T(h=h₀)}

            - для процедур

{K_T(h=H)} P_j(a₁,a₂, . . . ,a_nj){K_T(h=f_j(H,a₁,a₂, . . .,a_nj))}

инициализация m:=0

{T} Q {K_НМЦ(h=Ø)}

{T} Q {m=0}

Q: m:=0

wp(“m:=0”,m=0) = 0=0 = T

Инвариант класса.

Какое должно быть отношение между переменными класса.

I = 0£m<160 Ù (N_i,j : i¹j Ù 0£i<m Ù 0£j<m : b[i] = b[j] = 0

{I} Q_{содерж.} {I Ù K_НМЦ(x=iÎh)}

Само множество не меняется.

Преобразуем:

{I} Q_{содерж.} {I Ù x= $k: 0£k<m: b[k]=i)}

Заменим константу переменной:

Inv:

0£j£m Ù x:=$k: 0£k<j: b[k]=i

огр: m-j

охр: j¹m

j,x:=j+1,xÚb[j]=i

инициализация: j,x:=0,F

 j,x:=0,F

     do

         j¹m ® j,x:=j+1,x Ú b[j]=i

     od

Процедура добавления элемента

{I (K_НМЦ(hÚ{i}))} Ù K_НМЦ(h=H)}

     Q_{добавления}

{I Ù K_НМЦ(h=HÚ{i})}

{(iÎb Ù 0£m£100 Ú iÏb Ù 0£m+1£100) Ù m=M Ù b=B}

{0£m£100 Ù (iÎb Ù m£M Ù b=B Ú iÏb Ù m=M+1 Ù b[0:M-1]=B[0:M-1] Ù b[0:m-1]=i)}

Q_{добавления} содержит (i,x)

if

  x=T ® SKIP

 x=F ® m,b[m]:=m+1,i

fi

Удаление

{ I Ù K_НМЦ(h=H)} Q_{удаления} {K_НМЦ(h=H {i})}

{I Ù m=M Ù b=B}  Q_{удаления} {k: 0£k<m: b[k]=i Ù (m=M Ù b=B Ú m=M-1 Ù k: 0£k<m: (b[k]=B[k] Ú b[k]=B[M-1] Ù B[k] = i))}

Q_{удаления} содержит (i,x);

If

      x=F ® SKIP

            x=T ® Sц

fi

В лекции "Воспалительные заболевания кишечника" также много полезной информации.

Inv:

0£j£m Ù k: 0£k<j: (b[j]¹i Ù (b[k]=B[k] Ú b[k]=B[M-1] Ù B[k]=i))

Если это все доказано, то соответственно доказана и правильность представления данных.

Х – абстрактная программа

Х’ – конкретная программа

Х’ получаем из Х