- •8.1. Определение синтаксиса
- •8.1.1. Схема трансляции программы
- •8.2. Сравнение синтаксиса sml и ламбда-исчисления
- •8.2.1. Обозначения бнф
- •8.2.2. Синтаксис ламбда-исчисления
- •8.2.3. Синтаксис sml
- •9.1. Обобщенные требования к описанию языков программирования
- •9.2. Семантика языка программирования
- •9.3.1. Последовательность изложения теории вычислений д. Скотта
- •9.3.2. Определения способов комбинирования доменов
- •9.4. Формализация семантики языка функционального программирования sml
- •9.3. Теория вычислений д. Скотта
- •9.4.1. Порядок построения формальной модели семантики языка программирования sMalL согласно ранее представленному формальному описанию синтаксиса языка в терминах бнф
- •9.4.2. Вычислительная модель на основе состояний программы языка sMalL
- •9.5. Описание семантических предложений
- •9.5.1. Семантические предложения для выражений
- •9.5.2. Семантические предложения для команд
- •9.5.3. Семантические предложения для денотатов
9.5.2. Семантические предложения для команд
Приведем семантические предложения для команд языка программирования SMalL:
С : Com -> [State -> [ State + {error}]].
Из приведенного соотношения следует, что вычисление значения команды языка программирования SMalL приводит, вообще говоря, к изменению состояния, причем возможна ситуация (например, несоответствие типов в ходе присваивания), при которой вырабатывается ошибка.
9.5.3. Семантические предложения для денотатов
В соответствии с намеченной схемой рассуждений перейдем к описанию семантических предложений, которые описывают значение конкретных денотатов (т.е. правильно построенных конструкций) языка SMalL.
1. Семантические предложения для денотатов констант целочисленного типа языка SMalL:
E[0]s = (0,s);
E[1]s = (1,s);
Как видно из приведенных соотношений, денотатами констант целочисленного типа являются значения этих констант (в форме упорядоченных пар вида "значение"-"состояние"), причем смены состояния программы не происходит.
2. Семантические предложения для денотатов констант логического типа языка SMalL:
E[true]s = (true,s);
E[false]s = (false,s);
Как видно из приведенных соотношений, денотатами констант логического типа являются значения этих констант (в форме упорядоченных пар вида "значение"-"состояние."), причем смены состояния программы не происходит.
3. Семантическое предложение для денотатов идентификаторов языка SMalL:
E[I]s = (m,I=unbound) error, -> (m,I,s).
Как видно из приведенного соотношения, при возможности связывания денотатами идентификаторов являются идентификаторы, связанные со значениями (в форме упорядоченных троек вида "значение в памяти"-"идентификатор"-"состояние"), причем смены состояния программы не происходит, а при невозможности - выдается сообщение об ошибке.
4. Семантические предложения для денотатов выражений языка SMalL
4.1. Денотатом отрицания выражения является отрицание его значения; причем состояние программы изменяется. В случае несоответствия типов или небулевости выражения генерируется сообщение об ошибке.
E[-E]s=(E[E]s=(v,s'))
(isBool -> (not v,s'),error,error;
4.2. Денотатом присваивания является присвоенное значение в новом состоянии. В случае несоответствия типов генерируется сообщение об ошибке.
E[E1=E2]s=(E[E1]s=(v1,s1)) ->
(E[E2]s1= (v2,s2)) ->
(v1 = v2,s2),error),error;
4.3. Денотатом сложения является значение суммы в новом состоянии. В случае несоответствия типов генерируется сообщение об ошибке.
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.
5. В качестве упражнения предлагается самостоятельно разработать семантические предложения для денотатов команд языка программирования SMalL.
Выводы по лекции 9
В ходе лекции была представлена классификация подходов к семантике языков программирования, признан целесообразным денотационный подход, который проиллюстрирован на примере языка SMalL - ограниченного подмножества SML.
По итогам обсуждения можно сделать следующие выводы:
семантика языков функционального программирования достаточно близка к семантике формальных теорий, на которых они основаны (в частности, это справедливо для ламбда-исчисления и языка SML);
теория вычислений является актуальной и адекватной формализацией семантики;
денотационный подход является наиболее целесообразным для моделирования семантики языков программирования.
Для более подробного самостоятельного ознакомления с тематикой лекции рекомендуется следующий список источников: [24,40,42,52,67,70].
