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

{R: s = (Si: 1£i£10: b[i])}

Для того, чтобы доказать, что P - инвариант этого цикла, нам надо показать, что выполняются условия (11.4) 1-3. То, что P выполняется перед входом в цикл, доказать нетрудно. Для этого достаточно подставить в P значения i и s и учесть, что запись

(S k: i+1£k£10: b[k])

при i=10 даст 0.

Докажем, что выполняется условие (11.4) 2., т.е.

"k: 0£k£10: {PÙB_k } S {P},

где B_k = k+i=10 Ù i ³1; s: s:=s+b[i]; i:=i-1.

Это несложно сделать с помощью метода математической индукции.

Теперь нам осталось показать (11.4)3, что

PÙØBBÞR,

это условие можно записать так

PÙi<1 ÞR.

Учитывая, что в условии Р переменная i от 0 до 10, следовательно i<1, только при i=0. Отсюда, поставив в Р значение i=0, получим требуемое утверждение R.

Теперь, имея представление о семантике основных операторов языка Pascal, рассмотрим,что же нам дает такое понимание семантики для создания программ? Здесь, конечно, уместно было бы спросить, что мы понимаем под словами “создание программ”? Но мы ответим на этот вопрос чуть позже. А пока вернемся к нашим программам 9.1 и 10.1 и попытаемся на них понять, что же нам дает знание семантики.

Перепишем программу из примера 9.1, но в качестве комментариев будем записывать предусловия и постусловия для операторов этой программы. Результат этого преобразования показан на рис. 11.1.

Program Harmonic (input, output);

{ Предусловие: (nÎ N)Ù(n>0);

Постусловие: s = }

var n, i : integer;

s : real;

begin

{ T }

write(’Введите значение n =’);

readln( n ); { nÎ N }

if n>0 then

begin {(nÎ N)Ù(n>0)}

s:=0 ;

i:=1; {i=1 Ù s=0 Ù n>0}

while i£n do