2.2. Семантика

Семантика — это смысл высказывания (программы) в языке (программи­рования).

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

The pig is in the pen. (Свинья в загоне.)

The ink is in the pen. (Чернила в ручке.)

Нужно обладать достаточно обширными общими знаниями, не имеющи­ми никакого отношения к построению английских фраз, чтобы знать, что «реп» имеет разные значения в этих двух предложениях («загон» и «ручка»).

Формализованная нотация семантики языков программирования выходит за рамки этой книги. Мы только кратко изложим основную идею. В любой точ­ке выполнения программы мы можем описать ее состояние, определяемое: (1) указателем на следующую команду, которая будет выполнена, и (2) содержимым памяти программы. Семантика команды задается описанием изменения состо­яния, вызванного выполнением команды. Например, выполнение:

а:=25

заменит состояние s на новое состояние s', которое отличается от s только тем, что ячейка памяти а теперь содержит 25.

Что касается управляющих операторов, то для описания вычисления используется математическая логика. Предположим, что мы уже знаем смыслы двух операторов S1 и S2 в произвольном состоянии s. Обозначим это с по­мощью формул р (S1, s) и р (S2, s) соответственно. Тогда смысл if-оператора:

if С then S1 elseS2

задается формулой:

(C(s)=>p(S1,s))&((-C(s)=>p(S2,s))

Если вычисление С в состоянии s дает результат истина, то смысл if-опера­тора такой же, как смысл S1; в противном случае вычисление С дает результат не истина и смысл if-оператора такой же, как у S2.

Как вы можете себе представить, определение семантики операторов цик­ла и вызовов процедур с параметрами может быть очень сложным. Здесь мы удовлетворимся неформальными объяснениями семантики этих конструк­ций языка, как их обычно описывают в справочных руководствах:

Проверяется условие после if; если результат — истина, выполняется сле­дующий после then оператор, иначе выполняется оператор, следующий за else.

Формализация семантики языков программирования дает дополнитель­ное

преимущество — появляется возможность доказать правильность про­граммы. По сути, выполнение программы можно формализовать с помощью Кксиом, которые описывают, как оператор преобразует состояние, удовлетво­ряющее утверждению (логической формуле) на входе, в состояние, которое Удовлетворяет утверждению на выходе. Смысл программы «вычисляется» пу-тем построения входных и выходных утверждений для всей программы на ос­нове утверждений для отдельных операторов. Результатом является доказа­тельство того, что если входные данные удовлетворяют утверждению на входе, то выходные данные удовлетворяют утверждению на выходе.

Конечно, «доказанную» правильность программы следует понимать лишь относительно утверждений на входе и выходе, поэтому не имеет смысла доказывать, что программа вычисляет квадратный корень, если вам нужна программа для вычисления кубического корня! Тем не менее верификация про­граммы применялась как мощный метод проверки для систем, от которых требуется высокая надежность. Важнее то, что изучение верификации поможeт вам писать правильные программы, потому что вы научитесь мыслить, исходя из требований правильности программы. Мы также рекомендуем изучить и использовать язык программирования Eiffel, в который включена под­держка утверждений (см. раздел 11.5).