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

begin s:=s+1/i ; i:=i+1 end

{i=n , , n>0};

writeln (’Сумма’, п , ’ членов

гармонического ряда =’’, s)

end {}

else {n£0} writeln (’Ошибка в исходных данных.

Должно быть’, n,’ >0’)

end {}

Рис. 11.1.

В первом комментарии сформулированы пост- и пред- условия, определяющие множество допустимых исходных данных и множество возможных результатов. Комментарий {T} между строками 2 и 3 утверждает, что в этой точке программы допустимо любое состояние. Действительно, мы ничего пока еще не можем сказать в этой точке о значениях переменных этой программы.

Однако, после оператора readln (n) (строка 4) мы уже можем утверждать, что nÎ N, т.е. целое. Как Вы уже, наверное, изучали на семинарских занятиях, Pascal - это строго типизированный язык программирования. Это означает, что каждой переменной в программе как бы сопоставляется предикат, определяющий тип этой переменной. Всякий раз, когда происходит запись нового значения в эту переменную, происходит вычисление значения этого предиката. Если оно T, то запись выполняется, если F, то выдается сообщение об ошибке, и выполнение программы прекращается. Поэтому, после оператора readln (n), т.е. после его нормального завершения, мы можем быть уверены, что n - целое значение. Но мы ничего не можем сказать о величине этого значения. Поэтому, нам надо убедиться,что n > 0 , прежде чем начать вычисления.

В строке 5 логическое выражение n>0 обеспечивает проверку исходных данных на соответствие предусловию программы. Поэтому, после строки 5 мы можем быть уверены, что любое состояние, полученное в этой точке, будет удовлетворять предикату, написанному в виде комментария - {(nÎ N)Ù(n>0)}.

Комментарий в конце 7 строки определяет состояния вычислительного процесса непосредственно перед входом в цикл. Комментарий после заголовка цикла (строка 8) - { s=Sk : 0<k<i : 1/k} - определяет инвариант цикл. То, что это действительно так, мы убедились ранее, при рассмотрении семантики цикла.

Комментарий после строки 9 определяет состояние вычислительного процесса, непосредственно после окончания цикла. Он как раз утверждает то, что в этом состоянии переменная s будет иметь в качестве своего значения сумму ряда .

Комментарий в строке 10, после end показывает, что в этой точке состояние вычислительного процесса не изменится, если не принимать в расчет переменную П - указатель номера выполняемого оператора (см. лекцию 2).

Комментарий в строке 11 утверждает, что в этой точке у любого состояния вычислительного процесса n£0. Ну и , наконец, последний комментарий утверждает, что в любом заключительном состоянии вычислительного процесса, соответствующего корректным исходным данным (предусловие выполнено), в этой программе , т.е. постусловие для программы выполнено.

Если теперь сравнить программу на рис. 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 сделано наоборот.

Итак, мы обнаружили с Вами три разных формы представления, вообще говоря, одной и той же программы:

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