Предыдущая страница реферата | 1  2  3  4  5  6  7  8  9  10  11 | Следующая страница реферата

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) º 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:=E1 to E2 do S; (for i:=E1 downto E2 do S)

repeat S1 ; S2 ; … ; Sk  until B;

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

Рекомендуем скачать другие рефераты по теме: новшество, конспект.





Предыдущая страница реферата | 1  2  3  4  5  6  7  8  9  10  11 | Следующая страница реферата