Предыдущая страница реферата | 2  3  4  5  6  7  8  9  10  11  12 | Следующая страница реферата

$ 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, приведенному на рис. 11.3, инвариант выглядит так:

P: s=(Pk: 1£k<i: k))                   (11.3)

где s=Pk: 1£k<i :k означает .

Таким образом, мы можем добавить к условию (11.1) утверждение

("i: 0£i<k: PÙBB Þ (IF, P)) Ù (P Ù ØBB) Þ R ,

где P - инвариант цикла.

Другими словами, если P - инвариант, то он должен удовлетворять следующим условиям (11.4):

P должен выполняться непосредственно перед входом в цикл.

"i: 1£i£n: {PÙBi} Si {P}.

P Ù ØBB Þ R

В итоге получаем:

wp(DO, R) = $k: k³0: Ck(R) Ù ("i: 0£i<k: PÙBB Þ (IF, P)) Ù (P Ù ØBB Þ R) ,

где P - инвариант цикла.

Заметим, что не любое утверждение на множестве состояний итераций цикла является инвариантом цикла. Инвариант должен конструктивно помогать доказательству корректности цикла, т.е. что цикл заканчивается, т.е.

P Þ wp(DO, P Ù ØBB)                         (11.5)

и что заканчивается в состоянии, удовлетворяющем R, т.е.

(P Ù ØBB) Þ R                         (11.6)

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





Предыдущая страница реферата | 2  3  4  5  6  7  8  9  10  11  12 | Следующая страница реферата