Семантика оператора "case".
    Одной из форм оператора выбора в языке Pascal является оператор сase. Синтаксис этого оператора приведен ниже.
    сase of
    : {; :}
    end
    Например:
    сase i mod 3 of
    0: m:=0;
    1: m:=-1;
    2: m:=1;
    end
    nase sym of
    '=': k:=k+1;
    '*', '+', '/', '-': ;
    '!': l:=l+1;
    ':', ';': p:=p+1;
    end
    3. сase день of
    ПН, ВТ, СР, ЧТВ, ПТН: writeln('Рабочий день');
    СБ, ВСКР: writeln('Выходной день');
    end
    Ясно, что в этих примерах переменная i - типа integer, переменная sym - типа char, день - перечислимого типа (ПН, ВТ, СР, ЧТВ, ПТН, СБ, ВСКР).
    Действие оператора сase из примера 1 можно было бы описать так:
    if i mod 3=0 then m:=0 else
    if i mod 3=1 then m:=-1 else
    if i mod 3=2 then m:=1;
    Перепишем эту последовательность вложенных условных операторов в следующем виде:
    if
    i mod 3=0 ? m:=0;
    i mod 3=1 ? m:=-1;
    i mod 3=2 ? m:=1;
    end {if}
    В этой форме условия трех альтернатив просматриваются последовательно сверху вниз и выполняется первая альтернатива, условие которой выполнено.
    Обобщим теперь эту запись на большее число альтернатив следующим образом:
    if
    B1 ? S1;
    B2 ? S2;
    . . .
    Bk ? Sk
    end {if}
    В этом обобщении последовательно сверху вниз просматриваются логические выражения Bi и для того i, где первым будет получено значение T, будет выполнен оператор Si. Причем обязательно хоть одно Bi должно принять значение T. Эту обобщенную форму условного оператора обозначим IF. Отсюда получаем.
    Определение 11.1. Семантика оператора сase:
    wp(nase, R)=(? i: 1?i?k: Bi) ? (? i: 1?i?k: Bi ==> wp(Si, R))
    Отсюда должно быть видно, что:
    Всегда на текущем состоянии выполняется хотя бы одно Bi. Другими словами, предусловие этого оператора должно имплицировать любое Bi.
    Если на текущем состоянии выполняется Bi, то соответствующий Si перерабатывает это состояние в такое состояние, где должно выполняться постусловие R.
    Рассмотрим пример. Написать предусловие для оператора
    Snase:
    nase a of
    1: b:=c+a;
    2: b:=a+1;
    3: b:=a-c
    end
    такое, что если этот оператор начинает работать в состоянии, удовлетворяющем этому предусловию, то он обязательно закончит свою работу и после ее выполнения мы получим состояние, удовлетворяющее условию R ? b>1.
    Другими словами, надо вычислить
    wp(Snase, b>1).
    Выпишем в соответствии с определением
    wp(Scase , b>1) = ((a=1)?(a=2)?(a=3)) ?
    ((a=1) ==> wp(b:=c+a, b>1)) ?
    ((a=2) ==> wp(b:=a+1, b>1)) ?
    ((a=3) ==> wp(b:=a-c, b>1))
    Преобразуем каждый из предикатов (1)-(3) в соответствии с определением семантики оператора присваивания.
    Получим:
    (a=1) ==> (c+a>1) ? c>0
    (a=2) ==> (a+1>1) ? 3>1 ? T
    (a=3) ==> (a-c>1) ? c0)) ? (a=2) ? ((a=3) ? (c0 .
    Этот предикат выражает условие, что либо на текущем состоянии цикл заканчивается (член C0(R)), либо за одну итерацию цикла мы получим состояние, начиная с которого цикл закончится не более чем за k-1 итерацию (член wp(IF, Ck-1(R))).
    Таким образом, нижеприведенный предикат:
    ? k: k?0: Ck(R) (11.1)
    выражает условия 1,2 для циклов. ............