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

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

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

Кратко остановимся на наиболее значительных (с точки зрения целей этой книги) этапах эволюции теории и практики семантического анализа языков программирования.

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

В 1970;х гг. М. Гордоном (Michael J. С. Gordon) был исследован аппарат денотационной семантики применительно к языкам функционального программирования и сделан вывод об адекватности и практической эффективности применения этого подхода для решения поставленной задачи.

Параллельным направлением изучения семантики стал подход, исследовавший изменения, которые происходили в процессе работы программы на основе отслеживания смены состояний программы. Одним из практических результатов работ в этом направлении стала разработка П. Лендином (Peter J. Landin) семантики модели языка программирования в форме абстрактной машины, существенно использовавшей понятие состояния.

Альтернативный подход к формализации семантики (который осуществлен в рамках исследования так называемой операционной семантики языков программирования) привел к созданию Ч. Хоаром (Charles A. R. Ноаге) аксиоматического метода, моделирующего отношения и причинно-следственные связи, возникающие между операторами языка программирования.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Под функциональным пространством из домена в домен П)₂ будем понимать домен |П, Г)₂|, содержащий всевозможные функции с областью определения из домена Dj и областью значений из домена D₂:

[ D, —" D₂]={f | f: D, —" D₂}.

Под декартовым (или, иначе, прямым) произведением доменов D_t, D₂, …, D_n будем понимать домен всевозможных /?-ок вида.

[D₁xD₂x…xD_n]={(d₁xd₂x…xd_n) | d_{eD_v d₂eD₂, d_n …, eD_n}.

Под последовательностью D* будем понимать домен всевозможных конечных последовательностей вида.

d=(di, d₂,…, d_n).

из элементов d_t, d₂,…, d_n,… домена D, где n>0.

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

[D₁+D₂+…+D_n]={ (dp i) | djeDj, 0.

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

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

Прежде всего, рассмотрим синтаксис языка SmalL, т. е. перечислим основные типы конструкций, составляющих его. Язык SmalL содержит множество выражений Е, которые формализуются посредством БНФ в следующем виде:

Е := true | false | 0 | 1 111 ~Е | Е1=Е2 | Е1+Е2

Заметим, что выражения включают логические (true и false) и целочисленные (в ограниченном объеме: 0 и 1) константы, множество идентификаторов (I), а также операции отрицания (~Е), сравнения (Е1=Е2) и сложения (Е1+Е2). Кроме того, язык SmalL содержит множество команд С, которые формализуются посредством БНФ в следующем виде:

С := 1=Е | if (E)Cl else С2 | while (E) С | С1;С2

Заметим, что команды включают присваивание (1=Е), условие (if (E)Cl else С2), цикл с предусловием (while (E) С), а также последовательность команд (С1;С2). Деление синтаксиса языка SmalL на выражения и команды во многом является условным и служит иллюстративным целям.

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

Приведем порядок построения формальной модели семантики языка программирования SmalL согласно ранее представленному формальному описанию синтаксиса языка в терминах БНФ. Прежде всего, необходимо дать определение синтаксических доменов (т.е. доменов, характеризующих основные синтаксические категории) для идентификаторов (домен Ide), выражений (домен Ехр) и команд (домен Сот).

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

Заметим, что при выполнении программы (в частности, написанной на языке программирования SMalL) происходит изменение состояния, состоящего из памяти (m, memory), которая в простейшем случае характеризует соответствие идентификаторов и значений (т.е., по сути, связывание переменной со значением) либо имеет значение unbound (характеризующий отсутствие связи идентификатора со значением, т. е. аналогичный свободной переменной).

В соответствии с намеченной схемой рассуждений перейдем к описанию синтаксических доменов, которые в полной мере определяют синтаксис языка SMalL:

Ide = {I | I — идентификатор};

Com = {C | С — команда};

Exp = {E | E — выражение}.

Совокупность всех возможных идентификаторов языка SMalL организуется в домен Ide, команд — в домен Сот и, наконец, выражений — в домен Ехр.

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

Заметим, что состояние программы в произвольный момент времени определяется состоянием «памяти» абстрактной машины той или иной формы. При этом под памятью понимается отображение из домена идентификаторов в домен значений (т.е. аналог связывания переменной со значением в лямбда-исчислении). Для корректной обработки исключительных ситуаций, возникающих в случае свободных переменных, вводится дополнительный элемент unbound. Домен значений представляет собой дизъюнктную сумму доменов, содержащих существующие в языке SMalL типы lilt и Bool.

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

Е: Ехр —> |State —> [[Value х State]+{error}]];

Е[ E|s=(v, s'), если v — значение Е в s, s' — состояние после означивания;

E[E]s=error, если возникает ошибка несоответствия типов.

Из приведенных соотношений следует, что вычисление значения выражения языка программирования SMalL приводит к такому изменению состояния, что происходит связывание переменной со значением, либо.

(в случае невозможности связывания по причине несоответствия типов переменной и значения) вырабатывается ошибка. При этом состояние программы изменяется с s на s'. Приведем семантические предложения для команд языка программирования SMalL:

С: Com —" [State —" [ State+{error}]] .

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

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

Е [0] s=(0, s);

Е [1] s=(l, s);

Как видно из приведенных соотношений, денотатами констант целочисленного типа являются значения этих констант (в форме упорядоченных пар вида «значение» — «состояние»), причем смены состояния программы не происходит. Рассмотрим семантические предложения для денотатов констант логического типа языка SMalL:

Е [true] s=(true, s);

Е [false] s=(false, s);

Как очевидно из приведенных соотношений, денотатами констант логического типа являются значения этих констант (в форме упорядоченных пар вида «значение» — «состояние»), причем смены состояния программы не происходит. Рассмотрим семантическое предложение для денотатов идентификаторов языка SMalL:

Е 111 s=(m, I=unbound) error, —" (m, I, s).

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

Рассмотрим семантические предложения для денотатов выражений языка SMalL:

Е [~Е| s=(E | Е| s=(v, s')) (isBool —> (not v, s'), error, error;

E [E1=E2] s=(E [El]s=(vl, si)) (E [E2] sl=(v2, s2)) -> (vl=v2, s2),.

error), error;

E |E1+E2| s=(E [El] s=(vl, si)) -> (E |E2| sl=(v2, s2)).

(IsNum vl and IsNum v2 —" vl+v2, s2), error), error), error.

Проанализируем полученные соотношения. Денотатом отрицания выражения является отрицание его значения; причем состояние программы изменяется. В случае несоответствия типов или небулевости выражения генерируется сообщение об ошибке. Денотатом присваивания является присвоенное значение в новом состоянии. В случае несоответствия типов генерируется сообщение об ошибке. Денотатом сложения присваивания является значение суммы в новом состоянии. В случае несоответствия типов генерируется сообщение об ошибке.

В качестве упражнения предлагается самостоятельно разработать семантические предложения для денотатов команд языка программирования SMalL.

Итак, в параграфе представлена классификация подходов к семантике языков программирования, признан целесообразным денотационный подход, который проиллюстрирован на примере языка SMalL — ограниченного подмножества F#. По итогам обсуждения можно сделать следующие выводы:

• 1) семантика языков функционального программирования достаточно близка к семантике формальных теорий, на которых они основаны (в частности, это справедливо для лямбда-исчисления и языка F#);
• 2) теория вычислений является актуальной и адекватной формализацией семантики;
• 3) денотационный подход является наиболее целесообразным для моделирования семантики языков программирования.

Контрольные вопросы

Вопрос 1.

Вариант 1: в чем состоит основное назначение семантики?

• а) формализация вида и формы конструкций языка;
• б) формализация значения конструкций языка (+);
• в) формализация абстрактной машины для реализации языка.

Вариант 2: каковы требования к описанию формального языка?

• а) ясность, полнота, естественность, реализм (+);
• б) корректность, естественность, удобство использования;
• в) строгость, полнота, простота, эффективность.

Вариант 3: что из перечисленного является формализацией семантики?

• а) теория вычислений Д. Скотта (+);
• б) комбинаторная логика X. Карри;
• в) абстрактная машина П. Лендина (+).

Вопрос 2.

Вариант 1: какая из теорий не является формализацией семантики?

• а) аксиоматический метод Хоара;
• б) формы Бэкуса — Паура (+);
• в) метод индуктивных утверждений Р. Флойда.

Вариант 2: что понимается под семантикой?

• а) модель интерпретации абстрактного синтаксиса (+);
• б) модель реализации языка программирования;
• в) модель предметной области.

Вариант 3: на что ориентированы основные подходы к семантике?

• а) на компиляцию (+);
• б) интерпретацию (+);
• в) корректность типизации.

Вопрос 3.

Вариант 1: каковы виды семантик, ориентированные на интерпретацию?

• а) операционные, пропозиционные, денотационные (+);
• б) операционные, композиционные, денотационные;
• в) операционные, аппликативные, денотационные.

Вариант 2: какая формализация относится к денотационным семантикам?

• а) теория вычислений Д. Скотта (+);
• б) аксиоматический метод Ч. Хоара;
• в) абстрактная машина П. Лендина.

Вариант 3: какая формализация относится к операционным семантикам?

• а) теория вычислений Д. Скотта;
• б) аксиоматический метод Ч. Хоара;
• в) абстрактная машина П. Лендина (+).