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

на рис. 11.1 с двумя другими формами этой же программы, представленными на рис. 9.1 и рис. 9.2 , то мы должны согласиться, что это новая форма, новая программа. Согласно определению 9.1 один и тот же алгоритм может иметь разные программы, его реализующие. Различия между ними могут отражать различия во взглядах, потребностях создателя, исполнителя и пользователя этими программами. Что демонстрирует программа на рис. 11.1?

   Представим, что у компьютера, на котором мы будем исполнять эту программу, есть

кнопка, нажав которую, мы заставляем его выполнять очередной оператор программы и, выполнив его, остановиться;

после очередного нажатия, на специальном дисплее высветить текущие значения всех переменных программы.

Тогда, имея программу вычисления суммы 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=Семантика оператора “case”)  }

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)}.

Если Вам нужна помощь с академической работой (курсовая, контрольная, диплом, реферат и т.д.), обратитесь к нашим специалистам. Более 90000 специалистов готовы Вам помочь.
Бесплатные корректировки и доработки. Бесплатная оценка стоимости работы.

Поможем написать работу на аналогичную тему

Получить выполненную работу или консультацию специалиста по вашему учебному проекту
Нужна помощь в написании работы?
Мы - биржа профессиональных авторов (преподавателей и доцентов вузов). Пишем статьи РИНЦ, ВАК, Scopus. Помогаем в публикации. Правки вносим бесплатно.

Похожие рефераты: