Аннотирование цикла

Аннотирование цикла

Перед циклом

{Q}

{inv P: инвариант}

{bound t: ограничивающая функция}

do

B₁ ® S₁

        œB₂ ® S₂           

…       

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

        œB_n ® S_n

od

{R : постусловие}

Список условий для проверки цикла

1) Р истинно перед выполнением цикла

2) Р является инвариантом цикла {P Ù B_i} S_i {P}

3) Выполнение  P и невыполнение BB должно дать R: P Ù BB Þ R

4) Если цикл еще не закончен, то ограничивающая функция положительна:

P Ù BB Þ t>0

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

{P Ù B_i} t₁:=t;S₁ {t<t₁}

Пример: найти сумму элементов массива.

{T}

i,S := 10,0;

{inv P:0£i£10 Ù S=()}

  {bound t:i}

Рекомендация для Вас - Протокол состояния связей OSPF.

  do

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

od

{R: S=()}