Реферат: Семантика оператора case

Однако, как мы уже установили, оператор цикла вида (1) выражается через повторные выполнения оператора IF в соответствующей форме. Здесь уместно вспомнить, что при построении операции композиции повторения мы использовали операцию композиции выбора также.

Мы приходим к выводу, что все наши три вида операторов цикла сводятся к повторному выполнению соответствующего оператора IF. Назовем эту конструкцию, лежащую в основе всех этих операторов цикла, циклом вида DO. Ее вид представлен на рис. 11.5.

DO

if

B₁ ® S₁ ;

B₂ ® S₂ ;

. . .

B_n ® S_n

endif

ENDO

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

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

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

wp(DO, R)

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

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

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

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

C₀ (R)=ØBBÙR,

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

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

Обозначим

C₁ (R)= C₀ (R) Ú wp(IF, C₀ (R)),

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

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

C_k (R)= C₀ (R) Ú wp(IF, C_k-1 (R)), где k>0 .

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

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

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