Тема 6. Семантика мов програмування

Уявімо побудова денотаціонной семантики найважливіших функцій мови програмування SML.

Нагадаємо, що історія розвитку теорії та практики семантичного аналізу мов програмування була розглянута у вступній лекції.

Перш за все, розглянемо неформальну семантику мов програмування.

Для побудови адекватної і зручною у використанні семантики необхідно, перш за все, визначити критерії, що характеризують "хороший" мова програмування.

Спробуємо сформулювати узагальнені вимоги, пропоновані до опису мов програмування.

По-перше, необхідно вимагати від мови програмування дотримання принципу повноти, тобто оснастити його таким набором конструкцій, який дозволяє описати синтаксис (і семантику) всіх допустимих конструкцій мови без пропусків істотних аспектів.

По-друге, мова програмування повинна задовольняти інтуїтивного вимогу ясності, а саме, об'єктивно забезпечувати читабельність програм, а також легкість і результативність пошуку відповідей на питання, що виникають в процесі розробки програмних проектів.

Важливою характеристикою мови програмування є природність, під якою ми будемо розуміти інтуїтивну близькість мови термінології розробника, а також використання уніфікованих, стандартних, звичних позначень.

Нарешті, необхідно враховувати і такий важливий параметр, як реалізм, який розуміється як облік природних обмежень на середу реалізації мови програмування, а саме, обсяг оперативної пам'яті, час реакції і цілий ряд інших суттєвих факторів.

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

Перш за все, розширимо уявлення про семантику мови програмування (або формальної теорії) хоча і попереднім, але більш конкретним визначенням цього поняття.

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

Виявляється, все різноманіття можливих підходів до семантиці можна в основному уявити всього двома типами семантик, а саме, семантики, орієнтованими на компіляцію, і семантики, орієнтованими на інтерпретацію.

Надалі під підходами до семантиці, орієнтованими на компіляцію, будемо розуміти такі підходи, в яких семантика являє собою безліч перетворень над синтаксичної моделлю в тій чи іншій формі.

На відміну від попереднього підходу, під підходами до семантиці, орієнтованими на інтерпретацію, будемо розуміти такі підходи, в яких семантика являє собою безліч описаних на спеціально побудованому метамови перетворень синтаксично правильних конструкцій мови програмування.

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

Виділимо основні напрямки, що існують в рамках підходу до семантики, орієнтованого на інтерпретацію, і зв'яжемо їх з розглянутими нами в ході лекції напрямками досліджень.

Виявляється, існує три основних види семантик, орієнтованих на інтерпретацію.

По-перше, необхідно згадати про операційні семантика. Значення конструкцій мови в таких семантика виражається в термінах переходів тієї чи іншої абстрактної машини з одного стану в інший. В якості показових прикладів абстрактних машин можна привести, зокрема, так звану SECD-машину П. Лендіна, а також категоріальну абстрактну машину. Обидві формалізації будуть розглянуті детальніше в ході подальших лекцій.

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

Нарешті, найбільш значущим для нас типом семантик, орієнтованих на інтерпретацію, є денотаціонние семантики, в яких сенс конструкцій мови представляється в термінах абстракції функцій, що оперують станами програми. Зокрема, даний підхід ілюструє теорія обчислень Д. Скотта, заснована на семантичних доменах, яку ми і пропонуємо увазі читача.

Нагадаємо, що теорія обчислень Д. Скотта була створена до появи більшості сучасних мов програмування, а саме наприкінці 60-х років.

Суттєво, що саме ця теорія (на відміну від, скажімо, класичної логіки і ряду інших формальних систем) дозволяє провести адекватну (а саме, повну і несуперечливу) формалізацію семантики мов програмування.

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

Сформулюємо послідовність викладу теорії обчислень Д. Скотта.

Для побудови теорії обчислень необхідно, по-перше, перерахувати так звані стандартні, або, точніше, найбільш часто використовувані в рамках даної формалізації, домени.

Після перерахування стандартних доменів необхідно визначити так звані кінцеві домени, або, точніше, домени, елементи яких можна перерахувати явним чином.

Нарешті, після перерахування доменів перейдемо до визначення конструкторів доменів, під якими розуміються операції побудови нових доменів на основі наявних. Інакше кажучи, визначимо способи комбінування доменів.

Перерахувавши основні типи елементарних доменів, перейдемо до їх комбінуванню допомогою конструкторів.

Зауважимо, що, подібно ламбда-обчисленню та комбінаторної логіки, теорія обчислень має досить лаконічним набором способів комбінування доменів. Як ми побачимо далі, існує всього чотири типи конструкторів. Тим не менш, такий набір є цілком достатнім для побудови домену, моделює семантику як завгодно складної предметної області або мови програмування.

Наведемо визначення перерахованих способів комбінування доменів.

Під функціональним простором з домену D1 в домен D2 будемо розуміти домен [D1-> D2], що містить всілякі функції з областю визначення з домену D1 і областю значень з домену D2:

[D1 -> D2] = {f | f: D1 -> D2}.

Під декартовим (або, інакше, прямим) добутком доменів

D1, D2, ... Dn будемо розуміти домен всіляких n-ок виду

.

Під послідовністю D * будемо розуміти домен всіляких кінцевих послідовностей виду d = (d1, d2, ..., dn) з елементів d1, d2, ..., dn, ... домену D, де n> 0.

Нарешті, під діз'юнктной сумою будемо розуміти домен з визначенням

де приналежність елементів di компонентам Di однозначно встановлюється спеціальними функціями приналежності.

Поставимо задачу формалізації семантики мови функціонального програмування SML. Зазначимо відразу, що в рамках даного курсу буде розглядатися не все безліч можливих конструкцій даної мови, а досить обмежене (хоча й цілком достатня для ілюстрації основних ідей курсу) їх підмножина, яке умовно назвемо мовою програмування SMalL і будемо іменувати так надалі.

Перш за все, розглянемо синтаксис мови SMalL, тобто перерахуємо основні типи конструкцій, що складають його.

Мова SMalL містить безліч виразів E, які формалізуються за допомогою БНФ в наступному вигляді:

E :: = true | false | 0 | 1 | I |-E |

E1 == E2 | E1 + E2

Зауважимо, що вирази включають логічні (true і false) і цілочисельні (в обмеженому обсязі: 0 і 1) константи, безліч ідентифікаторів (I), а також операції заперечення (-E), порівняння (E1 == E2) і складання (E1 + E2).

Крім того, мова SMalL містить безліч команд С, які формалізуються за допомогою БНФ в наступному вигляді:

З :: = I = E | if (E) C1 else C2 |

while (E) C | C1; C2

Зазначимо, що команди включають присвоювання (I = E), умова

(If (E) C1 else C2), цикл з передумовою (while (E) C), а також послідовність команд (C1; C2).

Розподіл синтаксису мови SMalL на вираження і команди багато в чому є умовним і служить ілюстративним цілям.

Як уже зазначалося, в якості математичної формалізації, що моделює семантику мов програмування (зокрема, мови SMalL), буде використовуватися теорія обчислень Д. Скотта.

Наведемо порядок побудови формальної моделі семантики мови програмування SMalL згідно з раніше поданою формальному опису синтаксису мови в термінах БНФ.

Перш за все, необхідно дати визначення синтаксичних доменів (тобто доменів, що характеризують основні синтаксичні категорії) для ідентифікаторів (домен Ide), виразів (домен Exp) і команд (домен Com).

Далі, слід представити визначення обчислювальної моделі на основі синтаксичних доменів.

Потім необхідно перейти до визначення семантичних функцій (E для домену Exp, C для домену Com і т.д.), які відображають синтаксичні конструкції мови програмування до відповідних їм семантичні уявлення.

Нарешті, слід сформулювати визначення семантичних пропозицій в термінах зміни станів програми.

Зауважимо, що при виконанні програми (зокрема, написаної на мові програмування SMalL) відбувається зміна стану пам'яті (m, memory), яке в простому випадку характеризує відповідність ідентифікаторів і значень (тобто, по суті, зв'язування змінної із значенням), або має значення unbound (характеризує відсутність зв'язку ідентифікатора зі значенням, тобто аналог вільної змінної).

Відповідно до наміченої схемою міркувань перейдемо до опису синтаксичних доменів, які повною мірою визначають синтаксис мови SMalL:

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

Com = {C | C - команда};

Exp = {E | E - вираз}.

Сукупність усіх можливих ідентифікаторів мови SMalL організуємо в домен Ide, команд - в домен Com, і, нарешті, виразів - в домен Exp.

Далі, сформулюємо обчислювальну модель на основі станів програми мови SMalL, для наочності представивши її у вигляді такої таблиці 8.1:

Таблиця 8.1. Обчислювальна модель на основі станів програми мови SMalLПараметр Домен Співвідношення

Стан State (s) State = Memory

Пам'ять Memory (m) Memory = Ide -> [Value + {unbound}]

Значення Value (v) Value = Int + Bool

Зауважимо, що стан програми в довільний момент часу визначається станом "пам'яті" абстрактної машини тієї чи іншої форми. При цьому під пам'яттю розуміється відображення з домену ідентифікаторів в домен значень (тобто аналог зв'язування змінної зі значенням в ламбда-численні). Для коректної обробки виняткових ситуацій, що виникають у разі вільних змінних, вводиться додатковий елемент unbound. Домен значень являє собою діз'юнктную суму доменів, що містять існуючі в мові SMalL типи Int і Bool.

Відповідно до наміченої схемою міркувань перейдемо до опису семантичних пропозицій, які описують значення денотатів (тобто правильно побудованих конструкцій) мови SMalL.

Наведемо семантичні пропозиції для виразів мови програмування 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. Розглянемо семантичні пропозиції для денотатів констант цілочисельного типу мови SMalL:

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

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

Як видно з наведених співвідношень, денотатами констант цілочисельного типу є значення цих констант (у формі упорядкованих пар виду "значення" - "стан"), причому зміни стану програми не відбувається. Розглянемо семантичні пропозиції для денотатів констант логічного типу мови SMalL:

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

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

Як видно з наведених співвідношень, денотатами констант логічного типу є значення цих констант (у формі упорядкованих пар виду "значення" - "стан."), Причому зміни стану програми не відбувається. Розглянемо семантичне пропозицію для денотатів ідентифікаторів мови SMalL:

E [I] s = (m, I = unbound) error, -> (m, I, s).

Як видно з наведеного співвідношення, при можливості зв'язування денотатами ідентифікаторів є ідентифікатори, пов'язані зі значеннями (у формі упорядкованих трійок вигляду "значення в пам'яті" - "ідентифікатор" - "стан"), причому зміни стану програми не відбувається, а при неможливості - видається повідомлення про помилку.

Розглянемо семантичні пропозиції для денотатів виразів мови SMalL:

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.

Проаналізуємо отримані співвідношення.

Денотатом заперечення висловлювання є заперечення його значення; причому стан програми змінюється. У разі невідповідності типів або небулевості вираження генерується повідомлення про помилку.

Денотатом присвоювання є присвоєне значення в новому стані. У разі невідповідності типів генерується повідомлення про помилку.

Денотатом складання є значення суми в новому стані. У разі невідповідності типів генерується повідомлення про помилку.

В якості вправи пропонується самостійно розробити семантичні пропозиції для денотатів команд мови програмування SMalL.

Коротко резюмуємо підсумки лекції.

В ході лекції була представлена ​​класифікація підходів до семантиці мов програмування, визнаний доцільним денотаціонний підхід, який проілюстрований на прикладі мови SMalL - обмеженого підмножини SML.

За підсумками обговорення можна зробити наступні висновки:

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

теорія обчислень є актуальною та адекватною формалізацією семантики;

денотаціонний підхід є найбільш доцільним для моделювання семантики мов програмування.