Семантические предложения для денотатов

Семантические предложения для команд

Семантические предложения для выражений

Приведем семантические предложения для выражений языка программирования 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.

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.

По итогам обсуждения можно сделать следующие выводы:

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

2. теория вычислений является актуальной и адекватной формализацией семантики;

3. денотационный подход является наиболее целесообразным для моделирования семантики языков программирования.

Для более подробного самостоятельного ознакомления с тематикой лекции рекомендуется следующий список источников: [24,40,42,52,67,70].

Дата добавления: 2014-01-07