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

Одной из форм оператора выбора в языке Pascal является оператор сase. Синтаксис этого оператора приведен ниже.
сase of
: {; :}
end
Например:
сase i mod 3 of
0: m:=0;
1: m:=-1;
2: m:=1;
end
ñase 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(ñase, R)=($ i: 1£i£k: Bi ) Ù (" i: 1£i£k: Bi Þ wp(Si , R))
Отсюда должно быть видно, что:
Всегда на текущем состоянии выполняется хотя бы одно Bi . Другими словами, предусловие этого оператора должно имплицировать любое Bi .
Если на текущем состоянии выполняется Bi , то соответствующий Si перерабатывает это состояние в такое состояние, где должно выполняться постусловие 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(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) Ù (c<2))
Семантика оператора цикла.
Здесь нам надо определить, как оператор цикла в языке Pascal меняет состояние вычислительного процесса. Другими словами, если задано постусловие R, то каково должно быть для него предусловие wp, чтобы в результате выполнения оператора получить R.
Операторы цикла в любом языке программирования реализуют операцию композиции повторения (см. лекция 3). В языке Pascal есть три вида оператора цикла:
while B do S;
for i:=E1 to E2 do S; (for i:=E1 downto E2 do S)
repeat S1 ; S2 ; … ; Sk until B;
где B - логическое выражение,
E1 , E2 - выражения,
S1 ; S2 ; … ; Sk - операторы.
С циклом вида (1) мы уже встречались в примере 9.1 вычисления n членов гармонического ряда. Фрагмент программы (строки 5-8) показан на рис. 11.1
{Вычисление суммы ряда}
{Инициализация цикла}
s:=0;
i:=1;
{Вычисление суммы первых n членов гармонического ряда}
while i£n do begin s:=s+1;
i:=i+1 end {while}
Рис. 11.1.
На рис. 9.3 были показаны все состояния вычислительного процесса программы Harmonic для n=5. Фактически каждая итерация этого цикла представляет из себя выполнение оператора if_endif на рис. 11.2, а операторы в строках 5,6 устанавливают значения для s и i, необходимые для начала цикла.
if
B1 ® s:=s+1/i; i:=i+1;
. . . . .
B5 ® s:=s+1/i; i:=i+1;
endif ,
где "j: 1£j£n: Bj = i=j.
Рис. 11.2.
Оператор IF, представленный на рис. 11.2, надо выполнять до тех пор, пока для очередного значения i истинен хоть один Bi º i=n. Как только при очередном выполнении IF ни одно из условий не будет выполнено, то более повторять выполнение этого IF не надо.
Обозначим
BB=B1 Ú B2 Ú B3 Ú ... Ú Bk ,
тогда оператор IF на рис. 9.2 надо выполнять до тех пор, пока выполняется BB.
Теперь рассмотрим циклы вида (2). Для этого вернемся к примеру 10.1, программа для которого представлена на рис. 10.1. Интересующий нас в данный момент фрагмент дан на рис. 11.3.
begin fctrl:=1;
for i:=2 to n do fctrl:=fctrl*i
end {if n=0}
Рис. 11.3
Здесь был использован цикл вида (2). Все состояния вычислительного процесса, соответствующие этому циклу, были пока
заны на рис. 10.2. Там же, в колонке, где указан номер итерации, указано и условие, при выполнении которого надо выполнять тело цикла на данной итерации.
Рассмотрим оператор IF на рис. 11.4.
i:=2 ; if
B1 ® fctrl:=fctrl*i; i:=i+1;
B2 ® fctrl:=fctrl*i; i:=i+1;
. . . . .
B5 ® fctrl:=fctrl*i; i:=i+1
endif
где "k: 1£ k £5 Bk º i=k.
Рис. 11.4
Если его выполнять до тех пор, пока выполняется BB, то мы получим конструкцию, эквивалентную той, что показана на рис. 11.3 с той оговоркой, что значение параметра цикла i после выхода из цикла на рис. 11.3 считается не определенным. Для того, чтобы убедиться в эквивалентности этих конструкций, достаточно построить вычислительный процесс, соответствующий циклическому выполнению IF с рис. 11.4 и сравнить его с вычислительным процессом на рис.10.2.
Таким образом, мы видим, что циклы вида (2) тоже сводятся к последовательному выполнению операторов типа IF, пока выполняется условие BB.
Рассмотрим теперь циклы вида (3):
repeat S until B.
На интуитивном уровне действие операторов цикла этого вида можно описать так: после каждого выполнения оператора S надо проверять условие B. Если оно не выполняется, то надо выполнить S еще раз, если выполняется, то цикл заканчивается. Другими словами, оператор цикла вида (3) можно выразить оператор цикла вида (1) следующим образом:
repeat S until B;
º
S; while ØB do S.
Однако, как мы уже установили, оператор цикла вида (1) выражается через повторные выполнения оператора IF в соответствующей форме. Здесь уместно вспомнить, что при построении операции композиции повторения мы использовали операцию композиции выбора также.
Мы приходим к выводу, что все наши три вида операторов цикла сводятся к повторному выполнению соответствующего оператора IF. Назовем эту конструкцию, лежащую в основе всех этих операторов цикла, циклом вида DO. Ее вид представлен на рис. 11.5.
DO
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).

Внимание, отключите Adblock

Вы посетили наш сайт со включенным блокировщиком рекламы!
Ссылка для скачивания станет доступной сразу после отключения Adblock!

Скачать полную версию