КОНЦЕПТУАЛЬНЫЕ ОСНОВЫ И СЕМАНТИКА ОБЪЕКТНО-ОРИЕНТИРОВАННОГО ПОДХОДА

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

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

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

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

Другим аспектом сравнительного анализа стало сопоставление семантик подмножеств языков программирования F# и C# на основе общей теоретической формализации.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

[D|—>D2]={f|f: Dj—»D2}.

Под декартовым (или, иначе, прямым) произведением доменов Dlf Г)2, ..., Dn будем понимать домен всевозможных n-ок вида

[D1xD2x...xDn]={(dlxd2x...xdn)|dleDl,d2€D2,dneDn,...}.

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

d=(dlfd2.....dn)

из элементов dt, d2,..., dn,... домена D, где n>0.

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

[D,+ D2+...+Dn]={(di>i)|dieDi, 0

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

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

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

Язык C# содержит множество выражений Е, которые формализуются посредством БНФ в следующем виде:

Е true|false|0| 1 |I|! Е|Е 1==Е2|Е 1+Е2

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

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

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

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

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

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

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

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

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

Ехр ={Е|Е — выражение}.

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

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

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

Таблица 2.1

Вычислительная модель программы языка С# на основе состояний

Параметр

Домен

Соотношение

Состояние

State

(s) State=Memorv

Память

Memory

(m) Memory=Ide —»[Value+{unbound}]

Значение

Value

(v) Value=Int+Bool

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

Е : Exp —> [State —» [[ValuexState]+{error}]];

E[E]s=(v,s’),

если

v — значение Е в s,

s’- состояние после означивания;

E|E|s=error,

если возникает ошибка несоответствия типов.

Из приведенных соотношений следует, что вычисление значения выражения языка программирования C# приводит к такому изменению состояния, что происходит связывание переменной со значением либо (в случае невозможности связывания по причине несоответствия типов переменной и значения) вырабатывается ошибка. При этом состояние программы изменяется с s на s’.

Приведем семантическое предложение для команд языка программирования С#:

С:Сош —> [State —> [State-»-{error}]].

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

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

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

E[l]s=(l,s);

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

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

Е| false |s=( false, s);

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

Е[1] s=(m,I=unbound) error, —» (m,I,s).

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

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

E[!E]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=(v 1, si)) -> (E [E2| sl=

(v2, s2)) —> (IsNum vl and IsNum v2 —> vl=v2, s2),error),error),error.

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

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

Итак, представлена классификация подходов к семантике языков программирования, признан целесообразным денотационный подход, который проиллюстрирован примером языка C# — ограниченного подмножества С#.

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

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

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

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

Вопрос 1.

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

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

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

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

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

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

Вопрос 2.

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

  • а) наиболее часто используемые (+);
  • б) характеризующие стандартные операторы языка;
  • в) соответствующие международным стандартам.

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

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

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

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

Вопрос 3.

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

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

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

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

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

  • а) теория вычислений Д. Скотта;
  • б) аксиоматический метод Ч. Хоара;
  • в) абстрактная машина П. Лендина (+).
 
Посмотреть оригинал
< Пред   СОДЕРЖАНИЕ   ОРИГИНАЛ     След >