S1. Последовательность операторов Если {V} S1 {P1} и {P1} S2 {P} То {V} (S1; S2) {P}

Пример: {V?} gr:=gr-1; gl:=gl-1 {il-1 gl

W1. Цикл с условием продолжения без инициализации Если {I B} S {I} {I} while B do S endwhile {I B}

W2. Цикл с условием продолжения с инициализацией Если {V} инициализация {I} и {I B} S {I} и {I B} P То {V} (инициализация; while B do S endwhile) {P}

Пример: k=1 while (k n and A(k) x) do k:=k+1 endwhile Предусловие: n Z and n 0 Постусловие: n Z and k Z and 1 k n+1 and (k n and A(k)=x or k=n+1)

{n Z and n 0} k:=1 while k n and A(k) x do k:=k+1 endwhile {n Z and k Z and 1 k n+1 and (k n and A(k)=x or k=n+1)} n Z and k Z and 1 k n+1 I

{n Z and n 0} k:=1 { I } { I and k n and A(k) x} k:=k+1 { I } { I and (k n and A(k) x)} {n Z and k Z and 1 k n+1 and (k n and A(k)=x or k=n+1)}

Суждение 1 {n Z and n 0} { I k 1 } {n Z and n 0} {n Z and 1 Z and 1 1 n+1 }

Суждение 2 {n Z and k Z and 1 k n+1 and k n and A(k) x} k:=k+1 {n Z and k Z and 1 k n+1 } {n Z and k Z and 1 k n } k:=k+1 {n Z and k Z and 1 k n+1 } {n Z and k Z and 1 k n } {n Z and k Z and 1 k n+1 } k k+1

Суждение 3 {n Z and k Z and 1 k n+1 and not (k n and A(k) x)} {n Z and k Z and 1 k n+1 and (k n and A(k)=x or k=n+1)}

Метод индуктивных утверждений А – описывает свойства данных; С – утверждение о правильности. Пример 1

1.I=0, J=0. J=I*N=0*N=0 2.J=IN I n, J n J n =I n N I n+1 =I n +1 J n+1 =J n +N=I n N+N=(I n +1)N=I n+1 N 3. I=M J=IN=MN

Условия верификации: 1.iA i (X, Y, …) j A j (X, Y, …) 2.i -> j V e path (V) X=Y+1e path (X)=Y+1 e path (Y)=Y X=X+1; Y=Y+Y; X=X+Y-2 e path (X)=(X+1)+(Y+Y)-2 e path (Y)=Y+Y=2Y

3. 4. U ij :