Команда повторения

Команда повторения

Общий вид:             While B do S

do B ® S od

do

     B₁ ® S₁

   œ B₂ ® S₂  

   ....

   œ B_n ® S_n

od

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

Повторять следующие действия пока возможно выбрать команду B_i , которая истинна, и выполнить соответствующее S_i.

do  BB ® if

B₁ ® S₁

...

œB_n ® S_n

       fi

od

Введем команду повторения через слабейшее предусловие:

H_x(R) – предикат

Наш цикл завершиться за k или менее шагов при истинном R.

H₀(R)=ØВВÙR

Не все охраны ложные, R – истина.

H_k(R)= H₀(R)Ú wp(If, H_k-1(R))_k>0

H₁(R)= H₀(R)Ú wp(If, H₀(R))= H₀(R)Ú wp(If, ØВВÙR)

Wp( DO ,R)=$k:0£k: H_k(R)

Пример: посчитать сумму элементов массива b[0:10]

b[0:10]

i, S:=1,b[0];

do i<11 ® i, S:= i+1,S+b[i] od

{R:S=()}

Сформируем предусловие

Введем предикат Р:1 £ i £ 11 Ù S=()

Если Р истина перед циклом, перед каждым шагом цикла и после него, то Р истинно после цикла.

Нетрудно заметить, что

            РÙi³11 ÞR

{P=True}

i,S := 1,b[0];

{R} проверяем истинность Р

do

  i<11 ® {PÙi<11}i,S:=i+1,S+b[i]

  {P}

od

 {I³11 Ù P}        цикл завершился

 {R}

1. Р истинно перед циклом
2. P истинно перед каждым шагом

     Отсюда вывод: истинность Р и ложность охран позволяет заключить, что искомый результат R получен.

Доказательство:

1. Проверим истинность P после инициализации переменных

wp(“i,S:=1,b[0]”,P) = (1£1£11 Ù b[0] = ()) =

= (1£1£11 Ù b[0]=b[0]) = T

1. докажем истинность P после шага цикла, начавшемся при истинном Р и истинной охране.

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

=(1£i+1£11 Ù S+b[i]=())=

=(0£i£11 Ù S=) = T

1. Р может служить предусловием

P Ù i³11 Þ R

(1£i£11 Ù S=() Ù i³11 Þ ())=

= (i=11 Ù S=) Þ

Þ S=() = (вместо i подставляем 11)

видим, левая и правая части равны.

Предикат Р истинный перед и после выполнения каждого шага цикла, называется инвариантом цикла.

Введем функцию t, которая покажет, сколько шагов до конца цикла осталось.

t:=11-i

Это ограничивающая функция. Показывает верхнюю границу числа оставшихся шагов.

Составим программу, которая z ¬ a*b при b³0

{b³0}    

x,y,z := a,b,0;

do

     y>0 Ù чет(у) ® y,x :=y¸2, x+x

   œ нечет(у)     ® y,z :=y-1, z+x

od

{R:z=a*b}

Инвариант P: y³0 Ù z+x+y=a*b

1. Проверяем истинность Р после инициализации переменных

Wp(“x,y,z:=a,b,0”,P)=( (b³0)Ù(0+a*b=a*b) )=(b³0)

2. Перед шагом и после шага цикла

                                                                      Эти скобки раскрывать нельзя, но

а) z+x*y               z+(y/2)*(x+x)              т.к. у – четное, то можно раскрыть.

      до шага            после шага

б)    z+x*y               z+x+y-1*x=  z+y*x  

      до шага            после шага 

"3 - Основные характеристики флюидов" - тут тоже много полезного для Вас.

3. Истинность инварианта и ложность охран ® постусловие.

Р Ù Ø(у>0 Ù чет(у)) Ù Øнечет(y) =

= Р Ù (у£0)=(у£0 Ú Øчет(у) Ù четн(у) Ù Р)=

=( y£0 Ù чет(у) Ù Р)= ( y£0 Ù чет(у) Ù (у³0 Ù z+y*x=a*b))=

=(y=0 Ù z+y*x=a*b Þ z=a*b)

Ограничивающая функция t = y