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

Семантика оператора “ 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

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)) Ù

((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) º c<2

В итоге с использованием правил эквивалентных преобразований из таблицы 5.8 получим

((a=1) Ù (c>0)) Ú (a=2) Ú ((a=3) Ù (c<2))

Семантика оператора цикла.

Здесь нам надо определить, как оператор цикла в языке Pascal меняет состояние вычислительного процесса. Другими словами, если задано постусловие R, то каково должно быть для него предусловие wp, чтобы в результате выполнения оператора получить R.

Операторы цикла в любом языке программирования реализуют операцию композиции повторения (см. лекция 3). В языке Pascal есть три вида оператора цикла:

while B do S;

for i:=E₁ to E₂ do S; (for i:=E₁ downto E₂ do S)

repeat S₁ ; S₂ ; … ; S_k until B;

где B - логическое выражение,

E₁ , E₂ - выражения,

S₁ ; S₂ ; … ; S_k - операторы.

С циклом вида (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

B₁ ® s:=s+1/i; i:=i+1;

. . . . . <

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

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

Скачать