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

if

B1 ® S1;

B2 ® S2;

     . . .     

Bn ® Sn

endif

ENDO

Рис 11.5. Цикл вида DO.

Еще раз напомним, как он работает. Последовательно просматриваются сверху вниз условия Bi, и для первого выполненного условия выполняется надлежащий оператор Si. После этого опять cверху вниз, начиная с первого, просматриваются условия Bi. Выполнение оператора if заканчивается, когда при очередном просмотре ни одно Bi не будет выполняться.

Итак, для определения семантики трех видов оператора цикла нам достаточно определить семантику оператора DO! Теперь, придя к пониманию того, что в основе всех циклов лежит конструкция DO, попытаемся выписать ее семантику, то есть определить вид предиката

wp(DO, R)

Для любого цикла нам важно обеспечить выполнение двух условий:

Оператор цикла обязательно заканчивается.

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

Обозначим C0(R) предикат следующего вида:

C0(R)=ØBBÙR,

где BB - конъюнкция условий в операторе DO, а R - постусловие.

Очевидно, что C0(R) выражает условия 1,2 для оператора цикла, т.е. что цикл заканчивается (это описывает условие ØBB) и заканчивается в состоянии R (это описывает второй конъюнкт R).

Обозначим

C1(R)= C0(R) Ú wp(IF, C0(R)),

где wp(IF, C0(R)) - предусловие для оператора IF в операторе DO такое, что за одну итерацию цикла DO оператор IF переработает это состояние в состояние, удовлетворяющее условию C0(R), т.е. что цикл заканчивается  и заканчивается в состоянии R.

Таким образом, условие C1(R) описывает состояние, на котором цикл DO закончится не более чем за одну итерацию в состоянии, удовлетворяющем R. Теперь обобщим предикат C1(R) для случая не одной итерации цикла, а k итераций,

Ck(R)= C0(R) Ú wp(IF, Ck-1(R)), где k>0 .

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

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

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





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