Введение в теорию программирования. Функциональный подход


Семантика языков программирования - часть 2


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

В дальнейшем под подходами к семантике, ориентированными на компиляцию, будем понимать такие подходы, в которых семантика представляет собой множество преобразований над синтаксической моделью в той или иной форме.

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

Сразу отметим, что целям нашего курса в большей степени соответствует второй подход, как более универсальный в силу того обстоятельства, что в нем используется метатеория, т.е. формализация, моделирующая преобразования текста программ.

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

Оказывается, существует три основных вида семантик, ориентированных на интерпретацию.

Во-первых, необходимо упомянуть об операционных семантиках. Значение конструкций языка в таких семантиках выражается в терминах переходов той или иной абстрактной машины из одного состояния в другое. В качестве показательных примеров абстрактных машин можно привести, в частности, так называемую SECD-машину П. Лендина, а также категориальную абстрактную машину. Обе формализации будут рассмотрены подробнее в ходе дальнейших лекций.

Другим типом семантик, ориентированных на интерпретацию, являются так называемые пропозиционные семантики. В отличие от операционных семантик, значение конструкций языка в таких семантиках выражается в терминах множества формул, описывающих состояния объектов программы. В качестве примеров можно привести, в частности, аксиоматический метод Хоара и метод индуктивных утверждений Флойда.




Начало  Назад  Вперед



Книжный магазин