Команда повторения
Команда повторения
Общий вид: While B do S
do B ® S od
do
B1 ® S1
œ B2 ® S2
....
œ Bn ® Sn
od
Рекомендуемые материалы
Повторять следующие действия пока возможно выбрать команду Bi , которая истинна, и выполнить соответствующее Si.
do BB ® if
B1 ® S1
...
œBn ® Sn
fi
od
Введем команду повторения через слабейшее предусловие:
Hx(R) – предикат
Наш цикл завершиться за k или менее шагов при истинном R.
H0(R)=ØВВÙR
Не все охраны ложные, R – истина.
Hk(R)= H0(R)Ú wp(If, Hk-1(R))k>0
H1(R)= H0(R)Ú wp(If, H0(R))= H0(R)Ú wp(If, ØВВÙR)
Wp( DO ,R)=$k:0£k: Hk(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}
- Р истинно перед циклом
- P истинно перед каждым шагом
Отсюда вывод: истинность Р и ложность охран позволяет заключить, что искомый результат R получен.
Доказательство:
- Проверим истинность P после инициализации переменных
wp(“i,S:=1,b[0]”,P) = (1£1£11 Ù b[0] = (
)) =
= (1£1£11 Ù b[0]=b[0]) = T
- докажем истинность P после шага цикла, начавшемся при истинном Р и истинной охране.
wp(“i,S:=i+1,S+b[i]”,P)=
=(1£i+1£11 Ù S+b[i]=(
))=
=(0£i£11 Ù S=) = T
- Р может служить предусловием
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
