Семантика языков программирования
Аннотация: В лекции излагаются основополагающие принципы, история развития, существующие подходы и выразительные возможности семантического представления формальных теорий и языков программирования.
Представим построение денотационной семантики важнейших функций языка программирования SML .
Напомним, что история развития теории и практики семантического анализа языков программирования была рассмотрена во вступительной лекции.
Прежде всего, рассмотрим неформальную семантику языков программирования.
Для построения адекватной и удобной в использовании семантики необходимо, прежде всего, определить критерии, характеризующие «хороший» язык программирования .
Попытаемся сформулировать обобщенные требования, предъявляемые к описанию языков программирования.
Во-первых, необходимо потребовать от языка программирования соблюдения принципа полноты , т.е. оснастить его таким набором конструкций, который позволяет описать синтаксис (и семантику ) всех допустимых конструкций языка без пропусков существенных аспектов.
Во-вторых, язык программирования должен удовлетворять интуитивному требованию ясности , а именно, объективно обеспечивать удобочитаемость программ, а также легкость и результативность поиска ответов на вопросы, возникающие в процессе разработки программных проектов.
Немаловажной характеристикой языка программирования является естественность , под которой мы будем понимать интуитивную близость языка терминологии разработчика, а также использование унифицированных, стандартных, привычных обозначений.
Наконец, необходимо учитывать и такой важный параметр , как реализм , который понимается как учет естественных ограничений на среду реализации языка программирования, а именно, объем оперативной памяти , время реакции и целый ряд других существенных факторов.
После обсуждения концептуально важных требований к языкам программирования в целом перейдем к неформальному обсуждению семантического подхода, способного обеспечить реализацию этих требований.
Прежде всего, расширим представление о семантике языка программирования (или формальной теории) хотя и предварительным, но более конкретным определением этого понятия.
Семантикой будем называть интерпретацию (или, иначе, смысловое значение) абстрактного синтаксиса (а точнее, множества допустимых видов конструкций языка), представленное в терминах той или иной математически строгой формальной модели .
Оказывается, все многообразие возможных подходов к семантике можно в основном представить всего двумя типами семантик , а именно, семантиками, ориентированными на компиляцию , и семантиками, ориентированными на интерпретацию .
В дальнейшем под подходами к семантике, ориентированными на компиляцию , будем понимать такие подходы, в которых семантика представляет собой множество преобразований над синтаксической моделью в той или иной форме.
В отличие от предыдущего подхода, под подходами к семантике, ориентированными на интерпретацию , будем понимать такие подходы, в которых семантика представляет собой множество описанных на специально построенном метаязыке преобразований синтаксически правильных конструкций языка программирования.
Сразу отметим, что целям нашего курса в большей степени соответствует второй подход, как более универсальный в силу того обстоятельства, что в нем используется метатеория , т.е. формализация, моделирующая преобразования текста программ.
Выделим основные направления, существующие в рамках подхода к семантике, ориентированного на интерпретацию , и свяжем их с рассмотренными нами в ходе лекции направлениями исследований.
Оказывается, существует три основных вида семантик, ориентированных на интерпретацию .
Во-первых, необходимо упомянуть об операционных семантиках . Значение конструкций языка в таких семантиках выражается в терминах переходов той или иной абстрактной машины из одного состояния в другое. В качестве показательных примеров абстрактных машин можно привести, в частности, так называемую SECD-машину П. Лендина , а также категориальную абстрактную машину . Обе формализации будут рассмотрены подробнее в ходе дальнейших лекций.
Другим типом семантик, ориентированных на интерпретацию , являются так называемые пропозиционные семантики . В отличие от операционных семантик , значение конструкций языка в таких семантиках выражается в терминах множества формул, описывающих состояния объектов программы. В качестве примеров можно привести, в частности, аксиоматический метод Хоара и метод индуктивных утверждений Флойда.
Наконец, наиболее значимым для нас типом семантик, ориентированных на интерпретацию , являются денотационные семантики , в которых смысл конструкций языка представляется в терминах абстракции функций, оперирующих состояниями программы. В частности, данный подход иллюстрирует теория вычислений Д. Скотта , основанная на семантических доменах , которую мы и предлагаем вниманию читателя.
Напомним, что теория вычислений Д. Скотта была создана до появления большинства современных языков программирования, а именно в конце 60-х годов.
Существенно, что именно эта теория (в отличие от, скажем, классической логики и ряда других формальных систем) позволяет произвести адекватную (а именно, полную и непротиворечивую) формализацию семантики языков программирования.
Теория вычислений Д. Скотта основана на фундаментальном понятии домена , который будем пока неформально понимать как некоторый аналог множества , впрочем, в отличие от традиционных множеств , адекватно формализующий рекурсивно (т.е. на основе самоприменения) определенные функции и множества .
Сформулируем последовательность изложения теории вычислений Д. Скотта .
Для построения теории вычислений необходимо, во-первых, перечислить так называемые стандартные, или, точнее, наиболее часто используемые в рамках данной формализации, домены .
После перечисления стандартных доменов необходимо определить так называемые конечные домены , или, точнее, домены , элементы которых можно перечислить явным образом.
Наконец, после перечисления доменов перейдем к определению конструкторов доменов , под которыми понимаются операции построения новых доменов на основе имеющихся. Иначе говоря, определим способы комбинирования доменов .
Семантика языков программирования
Аннотация: В лекции излагаются основополагающие принципы, история развития, существующие подходы и выразительные возможности семантического представления формальных теорий и языков программирования.
Представим построение денотационной семантики важнейших функций языка программирования SML .
Напомним, что история развития теории и практики семантического анализа языков программирования была рассмотрена во вступительной лекции.
Прежде всего, рассмотрим неформальную семантику языков программирования.
Для построения адекватной и удобной в использовании семантики необходимо, прежде всего, определить критерии, характеризующие «хороший» язык программирования .
Попытаемся сформулировать обобщенные требования, предъявляемые к описанию языков программирования.
Во-первых, необходимо потребовать от языка программирования соблюдения принципа полноты , т.е. оснастить его таким набором конструкций, который позволяет описать синтаксис (и семантику ) всех допустимых конструкций языка без пропусков существенных аспектов.
Во-вторых, язык программирования должен удовлетворять интуитивному требованию ясности , а именно, объективно обеспечивать удобочитаемость программ, а также легкость и результативность поиска ответов на вопросы, возникающие в процессе разработки программных проектов.
Немаловажной характеристикой языка программирования является естественность , под которой мы будем понимать интуитивную близость языка терминологии разработчика, а также использование унифицированных, стандартных, привычных обозначений.
Наконец, необходимо учитывать и такой важный параметр , как реализм , который понимается как учет естественных ограничений на среду реализации языка программирования, а именно, объем оперативной памяти , время реакции и целый ряд других существенных факторов.
После обсуждения концептуально важных требований к языкам программирования в целом перейдем к неформальному обсуждению семантического подхода, способного обеспечить реализацию этих требований.
Прежде всего, расширим представление о семантике языка программирования (или формальной теории) хотя и предварительным, но более конкретным определением этого понятия.
Семантикой будем называть интерпретацию (или, иначе, смысловое значение) абстрактного синтаксиса (а точнее, множества допустимых видов конструкций языка), представленное в терминах той или иной математически строгой формальной модели .
Оказывается, все многообразие возможных подходов к семантике можно в основном представить всего двумя типами семантик , а именно, семантиками, ориентированными на компиляцию , и семантиками, ориентированными на интерпретацию .
В дальнейшем под подходами к семантике, ориентированными на компиляцию , будем понимать такие подходы, в которых семантика представляет собой множество преобразований над синтаксической моделью в той или иной форме.
В отличие от предыдущего подхода, под подходами к семантике, ориентированными на интерпретацию , будем понимать такие подходы, в которых семантика представляет собой множество описанных на специально построенном метаязыке преобразований синтаксически правильных конструкций языка программирования.
Сразу отметим, что целям нашего курса в большей степени соответствует второй подход, как более универсальный в силу того обстоятельства, что в нем используется метатеория , т.е. формализация, моделирующая преобразования текста программ.
Выделим основные направления, существующие в рамках подхода к семантике, ориентированного на интерпретацию , и свяжем их с рассмотренными нами в ходе лекции направлениями исследований.
Оказывается, существует три основных вида семантик, ориентированных на интерпретацию .
Во-первых, необходимо упомянуть об операционных семантиках . Значение конструкций языка в таких семантиках выражается в терминах переходов той или иной абстрактной машины из одного состояния в другое. В качестве показательных примеров абстрактных машин можно привести, в частности, так называемую SECD-машину П. Лендина , а также категориальную абстрактную машину . Обе формализации будут рассмотрены подробнее в ходе дальнейших лекций.
Другим типом семантик, ориентированных на интерпретацию , являются так называемые пропозиционные семантики . В отличие от операционных семантик , значение конструкций языка в таких семантиках выражается в терминах множества формул, описывающих состояния объектов программы. В качестве примеров можно привести, в частности, аксиоматический метод Хоара и метод индуктивных утверждений Флойда.
Наконец, наиболее значимым для нас типом семантик, ориентированных на интерпретацию , являются денотационные семантики , в которых смысл конструкций языка представляется в терминах абстракции функций, оперирующих состояниями программы. В частности, данный подход иллюстрирует теория вычислений Д. Скотта , основанная на семантических доменах , которую мы и предлагаем вниманию читателя.
Напомним, что теория вычислений Д. Скотта была создана до появления большинства современных языков программирования, а именно в конце 60-х годов.
Существенно, что именно эта теория (в отличие от, скажем, классической логики и ряда других формальных систем) позволяет произвести адекватную (а именно, полную и непротиворечивую) формализацию семантики языков программирования.
Теория вычислений Д. Скотта основана на фундаментальном понятии домена , который будем пока неформально понимать как некоторый аналог множества , впрочем, в отличие от традиционных множеств , адекватно формализующий рекурсивно (т.е. на основе самоприменения) определенные функции и множества .
Сформулируем последовательность изложения теории вычислений Д. Скотта .
Для построения теории вычислений необходимо, во-первых, перечислить так называемые стандартные, или, точнее, наиболее часто используемые в рамках данной формализации, домены .
После перечисления стандартных доменов необходимо определить так называемые конечные домены , или, точнее, домены , элементы которых можно перечислить явным образом.
Наконец, после перечисления доменов перейдем к определению конструкторов доменов , под которыми понимаются операции построения новых доменов на основе имеющихся. Иначе говоря, определим способы комбинирования доменов .