→ Пошук по сайту       Увійти / Зареєструватися
Знання Мова програмування C#

Семантика основних конструкцій мови програмування 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 #:

I de = {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 [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 (як метасередовищем), які принципово забезпечують можливість "занурення" у себе різних мов і підходів до програмування.

загрузка...
Сторінки, близькі за змістом