Семантика оператора “case”
Представим, что у компьютера, на котором мы будем исполнять эту программу, есть
кнопка, нажав которую, мы заставляем его выполнять очередной оператор программы и, выполнив его, остановиться;
после очередного нажатия, на специальном дисплее высветить текущие значения всех переменных программы.
Тогда, имея программу вычисления суммы n первых членов гармонического ряда в форме как на рис. 11.1, мы легко сможем проверить после каждого нажатия кнопки: действительно ли программа работает верно. Для этого достаточно подставить в предикат, определяющий текущее состояние, значения переменных из этого состояния, получить высказывания и вычислить его истинность. Если мы получим значение Т, то программа работает правильно, если F, то не правильно.
Заметим также, что, зная семантику операторов, мы могли бы доказать, что в случае программы из примера 9.1, для каждого из предусловий соответствующий опреатор приводит состояние, удовлетворяющее требуемому постусловию. И, что в итоге, мы получим состояние, удовлетворяющее постусловию для программы.
Таким образом, мы приходим к выводу, что программа на рис. 11.1 отражает взгляд на программу, показанную на рис. 9.1, того, кто будет проверять правильность этой программы.
Определение 11.1. Назовем процесс формулировки пред и постусловий как для программы вцелом, так и для отдельных ее частей, вплоть до опраторов, процессом спецификации программы.
Определение 11.2. Набор пред и постусловий в порядке их выполнения, как для программы вцелом, так и для отдельных ее частей, вплоть до операторов, назовем спецификацией программы.
Теперь мы можем сказать, что на рис. 11.1 представлена программа с рис. 9.2 со спецификацией.
На рис. 11.2 показана программа и ее спецификация для примера 10.1. В отличие от программы на рис. 11.1, в этой программе, после проверки корректности исходных данных, мы сначала выдаем сообщение об ошибке и только потом приступаем к обработке. В программе на рис. 11.1 сделано наоборот.
Итак, мы обнаружили с Вами три разных формы представления, вообще говоря, одной и той же программы:
для пользовтеля, кто будет читать и стараться понять как работает эта программа;
для компьютера, который будет выполнять эту программу;
для того, кто будет проверять правильность этой программы.
Program Factorial (input, output);
{ Предусловие: (nÎ N)Ù(n ³ 0)
Постусловие: (Fctrl=) }
var i , n , fctrl : integer;
begin { T }
write(¢Введите значение n = ¢);
readln( n ); { nÎ N }
if n < 0 then { n < 0 }writeln (¢Ошибка: n не может быть < 0¢)
else
begin { n ³ 0 }
if n = 0 then {n=0} fctrl:=1 {n=0Ùfctrl=1Ù(i не определенно)}
else
begin { n > 0 }
fctrl : =1 ;
{n=0 Ù fctrl=1}
for i : =2 to n do fctrl : = fctrl * i
{"i: 2 £ i £ n : Pk : 1£k<i : k};
{ n>0 Ù fctrl=(Pi : 1£i<n : i) }
writeln (¢ При n = ¢ , n , ¢ n! = ¢ , fctrl )
end
{ n ³ 0 Ù fctrl= n! };
end
end {Program}
Рис. 11.2.
Упражнения:
{?} 1. if a=1 then b:=a else b:=a+1; {b=1} {i=n Ù j=m} |
wp (S5 , a > 0 Ù b > 0) = ? S5: if a > b then a:=a-b else if b < a then b:=b-a; |
2. if i=0 then j:=0 else j:=r; {?} |
wp (S6 , x £ y) = ? S6: if x > y then begin t:=x;x:=y;y:=t end; |
{i=n Ù j=m} if i=0 then j:=0; {?} |
Вычислить: wp(x:=2*y+3, х=13) wp(x:=х+y, х<2*y) wp(j:=j+1, 0<j Ù("i: 0 £ i £ j: b[i]=5)) wp(x:=х*y , х*y=c) |
4. if w £ r then begin r:=r-w; q:=q+1; end ; {q * w+r = x Ùr ³0} |
case c of ¢ + ¢ : p:=p+1; ¢ - ¢ : m:=m+1; ¢(¢, ¢)¢ : b:=b+1; ¢*¢,¢/¢ : p:=b+1; end {p>0, m>0, b=0} |
Цикл.
Проверка цикла.
Доказать, что Р до входа в цикл
"i: 1 £ i £ n : {PÙBi} S {P}
PÙØBBÞR
Доказать,что в следующих циклах Р - инвариант и цикл заканчивается в нужном состоянии R:
1.
{0 £ n }
i:=0 ;
{P: 0 £ i £ n Ù xÏ b [0: i-1]}
while (i < n) and (x¹ b[i]) do i:=i+1;
{R: (0 £ i £ n Ù x= b[i])Ú( i = n Ù xÏ b [0: i-1])}
2.
{0 < n }
i:=1 ;
{P: 0 < i £ n Ù ($p: i=2p)}
while 2*i £ n do i:=2*i ;
{R: 0 < i £ n< 2*i Ù ($p: i=2p)}.