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

 

Семантика основных конструкций языка программирования C#

Представим построение денотационной семантики важнейших конструкций языка программирования C#.
Напомним, что история развития теории и практики семантического анализа языков программирования были рассмотрены во вступительной лекции.
Процедура построения денотационной семантики основных конструкций языка программирования SML изложена в лекции 8.
Поставим задачу формализации семантики языка объектно-ориентированного программирования C#. Заметим сразу, что в рамках данного курса будет рассматриваться не все множество возможных конструкций данного языка, а некоторое весьма ограниченное (хотя и вполне достаточное для иллюстрации основных идей курса) их подмножество, которое условно назовем языком программирования C# и будем именовать так в дальнейшем.
Прежде всего, рассмотрим синтаксис языка C#, т.е. перечислим основные типы составляющих его конструкций.
Язык C# содержит множество выражений E, которые формализуются посредством БНФ в следующем виде:
E ::= true|false|0|1|I|!E|E1==E2|E1+E2
Заметим, что выражения включают логические (true и false) и целочисленные (в ограниченном объеме: 0 и 1) константы, множество идентификаторов (I), а также операции отрицания (!E), сравнения (E1==E2) и сложения (E1+E2).
Кроме того, язык C# содержит множество команд С, которые формализуются посредством БНФ в следующем виде:
С::=I=E | if(E)C1 else C2 |
while(E) C | C1;C2
Заметим, что команды включают присваивание I=E, условие if(E)C1 else C2, цикл с предусловием while(E) C, а также последовательность команд C1;C2.
Деление синтаксиса языка C# на выражения и команды во многом является условным и служит иллюстративным целям.
Как и ранее, в качестве математической формализации, моделирующей семантику языков программирования (в частности, языка C#), будет использоваться теория вычислений Д. Скотта.
Приведем порядок построения формальной модели семантики языка программирования C# согласно ранее представленному формальному описанию синтаксиса языка в терминах БНФ.
Прежде всего, необходимо дать определение синтаксических доменов (т.е. доменов, характеризующих основные синтаксические категории) для идентификаторов (домен Ide), выражений (домен Exp) и команд (домен Com).
Далее, следует представить определение вычислительной модели на основе синтаксических доменов.
Затем нужно перейти к определению семантических функций (E для домена Exp, C для домена Com и т.д.), которые отображают синтаксические конструкции языка программирования в соответствующие им семантические представления.
Наконец, следует сформулировать определение семантических предложений в терминах смены состояний программы.
Заметим, что при выполнении программы (в частности, написанной на языке программирования C#) происходит изменение состояния, состоящего из памяти (m, memory), которая в простейшем случае характеризует соответствие идентификаторов и значений (то есть, по сути, связывание переменной со значением) либо имеет значение unbound (характеризующее отсутствие связи идентификатора со значением, т.е. аналогичное свободной переменной).

В соответствии с намеченной схемой рассуждений, перейдем к описанию синтаксических доменов, которые в полной мере определяют синтаксис языка C#:
Ide ={I|I – идентификатор};
Com ={C|C – команда};
Exp ={E|E – выражение}.
Совокупность всех возможных идентификаторов языка C# организуем в домен Ide, команд – в домен Com, и, наконец, выражений – в домен Exp.
Далее, сформулируем вычислительную модель на основе состояний программы языка C#, для наглядности систематизировав ее в виде следующей таблицы:


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

Параметр

Домен

Соотношение

Состояние

State

(s) State = Memory

Память

Memory

(m) Memory = Ide [Value + (unbound)]

Значение

Value

(v) Value = Int + Bool

Заметим, что состояние программы в произвольный момент времени определяется состоянием «памяти» абстрактной машины той или иной формы. При этом под памятью понимается отображение из домена идентификаторов в домен значений (т.е. аналог связывания переменной со значением в ламбда-исчислении). Для корректной обработки исключительных ситуаций, возникающих в случае свободных переменных, вводится дополнительный элемент unbound. Домен значений представляет собой дизъюнктную сумму доменов, содержащих существующие в языке C# типы Int и Bool.
В соответствии с намеченной схемой рассуждений, перейдем к описанию семантических предложений, которые описывают значение денотатов (т.е. правильно построенных конструкций) языка C#.
Приведем семантические предложения для выражений языка программирования C#:
E : Exp -> [State ->
[[Value ( State] + {error}]];

E[E]s = (v,s’),
если
v – значение E в s,
s’– состояние после означивания;
E[E]s = error,
если возникает ошибка несоответствия типов.
Из приведенных соотношений следует, что вычисление значения выражения языка программирования C# приводит к такому изменению состояния, что происходит связывание переменной со значением, либо (в случае невозможности связывания по причине несоответствия типов переменной и значения) вырабатывается ошибка. При этом состояние программы изменяется с s на s’.
Приведем семантическое предложение для команд языка программирования C#:
С:Com->[State->[State+{error}]].
Из приведенного соотношения следует, что вычисление значения команды языка программирования C# приводит, вообще говоря, к изменению состояния, причем возможно возникновение ситуации (например, несоответствия типов в ходе присваивания), при которой вырабатывается ошибка.
В соответствии с намеченной схемой рассуждений, перейдем к описанию семантических предложений, которые описывают значение конкретных денотатов (т.е. правильно построенных конструкций) языка C#. Рассмотрим семантические предложения для денотатов констант целочисленного типа языка C#:
E[0]s=(0,s);
E[1]s=(1,s);
Как видно из приведенных соотношений, денотатами констант целочисленного типа являются значения этих констант (в форме упорядоченных пар вида «значение»-«состояние»), причем смены состояния программы не происходит. Рассмотрим семантические предложения для денотатов констант логического типа языка C#:
E[true]s=(true,s);
E[false]s=(false,s);
Как видно из приведенных соотношений, денотатами констант логического типа являются значения этих констант (в форме упорядоченных пар вида «значение»-«состояние»), причем смены состояния программы не происходит. Рассмотрим семантическое предложение для денотатов идентификаторов языка C#:
E[I]s=(m,I=unbound) error, -> (m,I,s).
Как видно из приведенного соотношения, при возможности связывания денотатами идентификаторов являются идентификаторы, связанные со значениями (в форме упорядоченных троек вида «значение в памяти»-«идентификатор»-«состояние»), причем смены состояния программы не происходит, а при невозможности – выдается сообщение об ошибке.
Рассмотрим семантические предложения для денотатов выражений языка C#:
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.
Проанализируем полученные соотношения.
Денотатом отрицания выражения является отрицание его значения; причем состояние программы изменяется. В случае несоответствия типов или небулевости выражения генерируется сообщение об ошибке.
Денотатом присваивания является присвоенное значение в новом состоянии. В случае несоответствия типов генерируется сообщение об ошибке.
Денотатом сложения является значение суммы в новом состоянии. В случае несоответствия типов генерируется сообщение об ошибке.
В качестве упражнения предлагается самостоятельно разработать семантические предложения для денотатов команд языка программирования C#.
В ходе лекции была представлена классификация подходов к семантике языков программирования, признан целесообразным денотационный подход, который проиллюстрирован примером языка C# – ограниченного подмножества C#.
Важнейший вывод, к которому мы неизбежно приходим к концу лекции, заключается в том, что семантики рассмотренных нами языков программирования SMalL и C# (которые являются подмножествами реальных языков SML и C#) имеют весьма много общего.
Более того, сходство семантики рассмотренных нами конструкций (команд и выражений) языков программирования SMalL и C# весьма прозрачно и очевидно. Для иллюстрации справедливости этого утверждения достаточно сопоставить результаты исследования семантики рассматриваемых языков программирования.
По результатам такого сопоставления можно прийти к закономерному выводу о том, что существует явное, непосредственное отображение конструкций рассмотренных языковых подмножеств друг в друга, причем это отображение носит взаимно однозначный характер.
Попутно мы можем сделать еще один важный вывод. Формализация денотационной семантики на основе доменов с помощью теории вычислений Д. Скотта является адекватной моделью семантики выражений и команд рассмотренных языков программирования (а также функционального и объектно-ориентированного подходов в целом). Таким образом, семантика языков функционального и объектно-ориентированного программирования достаточно близка к семантике формальных теорий, на которых они основаны (в частности, это справедливо для ламбда-исчисления и языков SML и C#). Кроме того, теория вычислений является актуальной и адекватной формализацией семантики, а денотационный подход – целесообразным для моделирования семантики различных языков программирования.
В завершение лекции хотелось бы указать на аналогию теории вычислений Д. Скотта и ламбда-исчисления (как метатеорий) со средой Microsoft .NET (как метасредой), которые принципиально обеспечивают возможность «погружения» в себя различных языков и подходов к программированию.

 

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