Реферат: Семантика оператора case
Как мы уже сказали, важно гарантировать, что цикл закончится и непременно в состоянии, удовлетворяющем постусловию. Обеспечивает эту гарантию особое утверждение (предикат), сохраняющий истинность на любом состоянии, порождаемом в цикле. Этот предикат называется инвариантом цикла или просто инвариантом. Другими словами, цикл 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)
В качестве упражнения докажите, что инварианты (11.2) и (11.3) обладают свойствами (11.5) и (11.6).
Рассмотрим следующий пример:
Доказать, что в следующем цикле P - инвариант и цикл заканчивается в нужном состоянии R.
{{T} - т.е. начинается с произвольного состояния}
i:=10, s:=0;
{P: 0£i£10 Ù s = (Sk: i+1£k£10: b[k])}