Построение циклов исходя из инвариантов

Построение циклов исходя из инвариантов и ограничений

Увеличить K, сохраняя j=(K mod 10)

if

       j < 9 ® K,j:=K+1,j+1

      j = 9 ® K,j:=K+1,0

fi

Правило:

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

{inv P}

Рекомендуемые материалы

{bound t}

 do

B ® уменьшить t, сохраняя Р

 od

{PÙ¬B}

Пусть нужно суммировать элементы массива

n³0  b[0:n-1]  

R: S=j: 0£j£n : b[j]

P:0£i£n Ù S=j: 0£j<i: b[j]

t: n-I

1. i,s:=0,0 – инициализация переменной, после которой P истина.
2. Нужно найти охраны.

P Ù ? Þ R    

P Ù I = n Þ R

B: i¹n

уменьшение ограничивающей функции

i:=i+1

S:=S+b[i] = j: 0£j<i+1: b[j]

S,i:= S+b[i],i+1

do

      i¹n ® i,S:=i+1,S+b[i]

od

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

1. Р истинно перед началом цикла

0£0£nÙ0=j: 0£j<0: b[j]=T

1. Р является инвариантом цикла wp(S_i,P)=P

Wp(“i,S:=i+1,S+b[i]”,P)=

=(0£i+1£n Ù S+b[i]= j: 0£j<i+1: b[j])

Это условие следует из Р и n¹i, отсюда следует что инвариант сохранился.

1. PÙ¬BBÞR   PÙi=nÞR

(0£n£nÙS)=(j: 0£j<n: b[j] )=(S=j: 0£j<n: b[j])

1. PÙi¹nÞt>0

PÙi¹nÞn-i>0[n>i]

В лекции "Условный оператор If." также много полезной информации.

0£i£nÙ i¹nÞn>i

1. Каждый шаг цикла ведет к его концу

{PÙ i¹n} t₁:=t; S_i {t<t₁}

{P i¹n} t₁:=n-i; i,S:=i+1,S+b[i] { t<t₁}

wp(“t₁:=n-i; i:=i+1”, n-i<t₁)=

wp(“t₁:=n-i”,n-i-1< t₁)= (n-i-1<n-i)=(1>0)=T