учебники, программирование, основы, введение в,

 

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

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


Перечислив основные типы элементарных доменов, перейдем к их комбинированию посредством конструкторов.
Заметим, что, подобно ламбда-исчислению и комбинаторной логике, теория вычислений обладает весьма лаконичным набором способов комбинирования доменов. Как мы увидим далее, существует всего четыре типа конструкторов. Тем не менее, такой набор является вполне достаточным для построения домена, моделирующего семантику сколь угодно сложной предметной области или языка программирования.
Приведем определения перечисленных способов комбинирования доменов.
Под функциональным пространством из домена  D1 в домен  D2 будем понимать домен [D1->D2], содержащий всевозможные функции с областью определения из домена D1  и областью значений из домена D2 :
[D1 -> D2] = {f | f : D1 -> D2}.
Под декартовым (или, иначе, прямым) произведением доменов
D1, D2, ... Dn будем понимать домен всевозможных n-ок вида
[D1 × D2 × ... × Dn]= {(d1 × d2 × ... × dn) | d1 D1, d2 D2, dn Dn ...,}.
Под последовательностью D* будем понимать домен всевозможных конечных последовательностей вида d=(d1,d2,...,dn) из элементов d1,d2,...,dn,... домена D, где n>0.
Наконец, под дизъюнктной суммой будем понимать домен с определением
[D1+D2+...+Dn]={ (di, i) | diDi, 0<i<n+1 },
где принадлежность элементов di компонентам Di однозначно устанавливается специальными функциями принадлежности.
Поставим задачу формализации семантики языка функционального программирования SML. Отметим сразу, что в рамках данного курса будет рассматриваться не все множество возможных конструкций данного языка, а весьма ограниченное (хотя и вполне достаточное для иллюстрации основных идей курса) их подмножество, которое условно назовем языком программирования SMalL и будем именовать так в дальнейшем.
Прежде всего, рассмотрим синтаксис языка SMalL, т.е. перечислим основные типы конструкций, составляющих его.
Язык SMalL содержит множество выражений E, которые формализуются посредством БНФ в следующем виде:
E ::= true | false | 0 | 1 | I | -E |
E1==E2 | E1+E2
Заметим, что выражения включают логические (true и false) и целочисленные (в ограниченном объеме: 0 и 1) константы, множество идентификаторов (I), а также операции отрицания (-E), сравнения (E1==E2) и сложения (E1+E2).
Кроме того, язык SMalL содержит множество команд С, которые формализуются посредством БНФ в следующем виде:
С ::= I=E | if (E) C1 else C2 |
while(E) C | C1;C2
Отметим, что команды включают присваивание (I=E), условие
(if (E) C1 else C2), цикл с предусловием (while(E) C), а также последовательность команд (C1;C2).
Деление синтаксиса языка SMalL на выражения и команды во многом является условным и служит иллюстративным целям.
Как уже отмечалось, в качестве математической формализации, моделирующей семантику языков программирования (в частности, языка SMalL), будет использоваться теория вычислений Д. Скотта.
Приведем порядок построения формальной модели семантики языка программирования SMalL согласно ранее представленному формальному описанию синтаксиса языка в терминах БНФ.
Прежде всего, необходимо дать определение синтаксических доменов (т.е. доменов, характеризующих основные синтаксические категории) для идентификаторов (домен Ide), выражений (домен Exp) и команд (домен Com).
Далее, следует представить определение вычислительной модели на основе синтаксических доменов.
Затем необходимо перейти к определению семантических функций (E для домена Exp, C для домена Com и т.д.), которые отображают синтаксические конструкции языка программирования в соответствующие им семантические представления.
Наконец, следует сформулировать определение семантических предложений в терминах смены состояний программы.
Заметим, что при выполнении программы (в частности, написанной на языке программирования SMalL) происходит изменение состояния памяти (m, memory), которое в простейшем случае характеризует соответствие идентификаторов и значений (то есть, по сути, связывание переменной со значением), либо имеет значение unbound (характеризующее отсутствие связи идентификатора со значением, т.е. аналог свободной переменной).
В соответствии с намеченной схемой рассуждений перейдем к описанию синтаксических доменов, которые в полной мере определяют синтаксис языка SMalL:
Ide =   {I | I - идентификатор};
Com =   {C | C - команда};
Exp =   {E | E - выражение}.
Совокупность всех возможных идентификаторов языка SMalL организуем в домен Ide, команд - в домен Com, и, наконец, выражений - в домен Exp.
Далее, сформулируем вычислительную модель на основе состояний программы языка SMalL, для наглядности представив ее в виде следующей таблицы:

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

Параметр

Домен

Соотношение

Состояние

State

(s) State=Memory

Память

Memory

(m) Memory = Ide -> [Value+{unbound}]

Значение

Value

(v) Value=Int+Bool

Заметим, что состояние программы в произвольный момент времени определяется состоянием "памяти" абстрактной машины той или иной формы. При этом под памятью понимается отображение из домена идентификаторов в домен значений (т.е. аналог связывания переменной со значением в ламбда-исчислении). Для корректной обработки исключительных ситуаций, возникающих в случае свободных переменных, вводится дополнительный элемент unbound. Домен значений представляет собой дизъюнктную сумму доменов, содержащих существующие в языке SMalL типы Int и Bool.
В соответствии с намеченной схемой рассуждений перейдем к описанию семантических предложений, которые описывают значение денотатов (т.е. правильно построенных конструкций) языка SMalL.
Приведем семантические предложения для выражений языка программирования SMalL:
E : Exp -> [State -> [[Value, State] +
{error}]];
E[E]s = (v,s'),
если v - значение E в s,
s'- состояние после означивания;
E[E]s = error,
если возникает ошибка несоответствия типов.
Из приведенных соотношений следует, что вычисление значения выражения языка программирования SMalL приводит к такому изменению состояния, что происходит связывание переменной со значением, либо (в случае невозможности связывания по причине несоответствия типов переменной и значения) генерируется сообщение об ошибке. При этом состояние программы изменяется с s на s'.
Приведем семантические предложения для команд языка программирования SMalL:
С : Com -> [State -> [ State + {error}]].
Из приведенного соотношения следует, что вычисление значения команды языка программирования SMalL приводит, вообще говоря, к изменению состояния, причем возможна ситуация (например, несоответствие типов в ходе присваивания), при которой вырабатывается ошибка.
В соответствии с намеченной схемой рассуждений перейдем к описанию семантических предложений, которые описывают значение конкретных денотатов (т.е. правильно построенных конструкций) языка SMalL. Рассмотрим семантические предложения для денотатов констант целочисленного типа языка SMalL:
E[0]s = (0,s);
E[1]s = (1,s);
Как видно из приведенных соотношений, денотатами констант целочисленного типа являются значения этих констант (в форме упорядоченных пар вида "значение"-"состояние"), причем смены состояния программы не происходит. Рассмотрим семантические предложения для денотатов констант логического типа языка SMalL:
E[true]s = (true,s);
E[false]s = (false,s);
Как видно из приведенных соотношений, денотатами констант логического типа являются значения этих констант (в форме упорядоченных пар вида "значение"-"состояние."), причем смены состояния программы не происходит. Рассмотрим семантическое предложение для денотатов идентификаторов языка SMalL:
E[I]s = (m,I=unbound) error, -> (m,I,s).
Как видно из приведенного соотношения, при возможности связывания денотатами идентификаторов являются идентификаторы, связанные со значениями (в форме упорядоченных троек вида "значение в памяти"-"идентификатор"-"состояние"), причем смены состояния программы не происходит, а при невозможности - выдается сообщение об ошибке.
Рассмотрим семантические предложения для денотатов выражений языка SMalL:
E[-E]s=(E[E]s=(v,s'))
(isBool -> (not v,s'),error,error;

E[E1=E2]s=(E[E1]s=(v1,s1)) ->
(E[E2]s1= (v2,s2)) ->
(v1 = v2,s2),error),error;

E [E1+E2]s = (E [E1] s=(v1,s1)) ->
(E [E2]s1 = (v2,s2)) ->
(IsNum v1 and IsNum v2 -> v1+v2,s2),error),
error),error.
Проанализируем полученные соотношения.
Денотатом отрицания выражения является отрицание его значения; причем состояние программы изменяется. В случае несоответствия типов или небулевости выражения генерируется сообщение об ошибке.
Денотатом присваивания является присвоенное значение в новом состоянии. В случае несоответствия типов генерируется сообщение об ошибке.
Денотатом сложения является значение суммы в новом состоянии. В случае несоответствия типов генерируется сообщение об ошибке.
В качестве упражнения предлагается самостоятельно разработать семантические предложения для денотатов команд языка программирования SMalL.
Кратко резюмируем итоги лекции.
В ходе лекции была представлена классификация подходов к семантике языков программирования, признан целесообразным денотационный подход, который проиллюстрирован на примере языка SMalL - ограниченного подмножества SML.
По итогам обсуждения можно сделать следующие выводы:

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

 

 
На главную | Содержание | < Назад....Вперёд >
С вопросами и предложениями можно обращаться по nicivas@bk.ru. 2013 г.Яндекс.Метрика