Семантика языков программирования

Семантика языков программирования

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

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

Попытаемся  сформулировать обобщенные требования, предъявляемые к описанию языков программирования.

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

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

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

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

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

Прежде  всего, расширим представление о семантике языка программирования (или формальной теории) хотя и предварительным, но более конкретным определением этого понятия.

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

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

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

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

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

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

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

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

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

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

Напомним, что теория вычислений Д. Скотта была создана до появления большинства современных языков программирования, а именно в конце 60-х годов.

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

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

Сформулируем  последовательность изложения теории вычислений Д. Скотта.

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

После перечисления стандартных доменов необходимо определить так называемые конечные домены, или, точнее, домены, элементы которых можно перечислить явным образом.

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

Перечислив основные типы элементарных доменов, перейдем к их комбинированию посредством конструкторов.

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

Приведем определения  перечисленных способов комбинирования доменов.

Под функциональным пространством из домена   D₁ в домен   D₂ будем понимать домен   [D₁->D₂], содержащий всевозможные функции с областью определения из домена   D1  и областью значений из домена  D₂:

[D₁ -> D₂] = {f | f : D₁ -> D₂}.

Под декартовым (или, иначе, прямым) произведением доменов

D₁, D₂, ... D_n будем понимать домен всевозможных n-ок вида

.

Под последовательностью   D* будем понимать домен всевозможных конечных последовательностей вида d=(d₁,d₂,...,d_n) из элементов d₁,d₂,...,d_n,... домена   D, где n>0 .

Наконец, под дизъюнктной суммой будем понимать домен с определением

,

где принадлежность элементов d_i компонентам D_i однозначно устанавливается специальными функциями принадлежности