Предыдущая страница реферата | 1  2  3  4  5 | Следующая страница реферата

2: b:=a+1;

3: b:=a-c

end

такое, что если этот оператор начинает работать в состоянии, удовлетворяющем этому предусловию, то он обязательно закончит свою работу и после ее выполнения мы получим состояние, удовлетворяющее условию R º b>1.

Другими словами, надо вычислить

wp(Sñase, b>1).

Выпишем в соответствии с определением

wp(Scase , b>1) = ((a=1)Ú(a=2)Ú(a=3)) Ù

((a=1) Þ wp(b:=c+a, b>1)) Ù

((a=2) Þ wp(b:=a+1, b>1)) Ù

((a=3) Þ wp(b:=a-c, b>1))

Преобразуем каждый из предикатов (1)-(3) в соответствии с определением семантики оператора присваивания.

Получим:

(a=1) Þ (c+a>1) º c>0

(a=2) Þ (a+1>1) º 3>1 º T

(a=3) Þ (a-c>1) º c0)) Ú (a=2) Ú ((a=3) Ù (c0 .

Этот предикат выражает условие, что либо на текущем состоянии цикл заканчивается (член C0(R)), либо за одну итерацию цикла мы получим состояние, начиная с которого цикл закончится не более чем за k-1 итерацию (член wp(IF, Ck-1(R))).

Таким образом, нижеприведенный предикат:

$ k: k³0: Ck(R)                           (11.1)

выражает условия 1,2 для циклов. Однако, он мало что нам дает для понимания внутреннего устройства цикла, семантики итераций.

Как мы уже сказали, важно гарантировать, что цикл закончится и непременно в состоянии, удовлетворяющем постусловию. Обеспечивает эту гарантию особое утверждение (предикат), сохраняющий истинность на любом состоянии, порождаемом в цикле. Этот предикат называется инвариантом цикла или просто инвариантом. Другими словами, цикл DO устроен таким образом, что состояния, которые мы получаем в конце каждой итерации, носят не произвольный характер, а подчиняются некоторому единому условию, которое называется инвариантом цикла.

Вернемся к нашим примерам 9.1 и 10.1. В примере 9.1 нетрудно заметить, что условие

s=(S k: 1£k£i: 1/k)                                 (11.2)

сохраняет истинное значение в течение всей работы цикла. Здесь запись

(S k: 1£k£i: 1/k)

Рекомендуем скачать другие рефераты по теме: решебник 10 класс, деятельность доклад.





Предыдущая страница реферата | 1  2  3  4  5 | Следующая страница реферата