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

end {if}

В этой форме условия трех альтернатив просматриваются последовательно сверху вниз и выполняется первая альтернатива, условие которой выполнено.

Обобщим теперь эту запись на большее число альтернатив следующим образом:

if

B₁ ® S₁ ;

B₂ ® S₂ ;

. . .

B_k ® S_k

end {if}

В этом обобщении последовательно сверху вниз просматриваются логические выражения B_i и для того i, где первым будет получено значение T, будет выполнен оператор S_i . Причем обязательно хоть одно B_i должно принять значение T. Эту обобщенную форму условного оператора обозначим IF. Отсюда получаем.

Определение 11.1. Семантика оператора сase:

wp(ñase, R)=($ i: 1£i£k: B_i ) Ù (" i: 1£i£k: B_i Þ wp(S_i , R))

Отсюда должно быть видно, что:

Всегда на текущем состоянии выполняется хотя бы одно B_i . Другими словами, предусловие этого оператора должно имплицировать любое B_i .

Если на текущем состоянии выполняется B_i , то соответствующий S_i перерабатывает это состояние в такое состояние, где должно выполняться постусловие R.

Рассмотрим пример. Написать предусловие для оператора

S_ñase :

ñase a of

1: b:=c+a;

2: b:=a+1;

3: b:=a-c

end

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

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

wp(S_ñase , b>1).

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

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

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

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