Опис семантичних речень

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

Синтаксис кортежу

(<вираз>,..., <вираз>) Приклад 1: (1, 2*1, 2*2*1) Приклад 2: (1, true, 0, false)

Синтаксис опису змінних і функцій

Опис змінної: <опис>::= val <ідентифікатор> = <вираз> Опис функції: <опис>::= fun <ідентифікатор> <ідентифікатор> = <вираз> Приклад 1. val x=2; Приклад 2. fun fact n = if n<2 then 1 else n * fact (n - 1); Приклад 3. fun f (x,y) = x*x + y*y;

3 види семантик:

1) операційні семантики – переходи абстрактної машин из одного стану в інший: SECD-машина, КАМ

2) пропозиційні семантики – множина формул, що описує стани програми: аксіоматичний метод Хоара і метод індуктивних тверджень Флойда

3) денотаційні семантики – абстракції функцій, що оперують станами програми: теорія обчислень Дана Скотта (семантичні домени)

8.3.1. Теорія обчислень Д.Скотта

Для побудови теорії необхідно:

1) перерахувати стандартні домени

2) визначити кінцеві домени

3) визначити конструктори доменів

4) комбінування доменів з використанням конструкторів (існує 4 типи конструкторів)

8.3.2. Визначення способів комбінування доменів

Означення 1. Під функціональним простором з домена D₁ в домен D₂ розумітимемо домен [D₁->D₂], що містить всі можливві функції з областю визначення з домена D₁ і областю значень з домена D₂:

[D₁ -> D₂] = {f | f: D₁ -> D₂}.

Означення 2. Під декартовим (або, прямим) добутком доменів

D₁, D₂,... D_n будемо розуміти домен всіх можливих n -ок виду

[D₁ × D₂ ×... × D_n]= {(d₁ × d₂ ×... × d_n) | d₁ Î D₁, d₂ Î D₂, d_n Î D_n...,}.

Означення 3. Під послідовністю D* будемо розуміти домен всіх можливих кінцевих послідовностей виду d=(d₁,d₂,...,d_n) з елементів d₁,d₂,...,d_n,... домену D, где n>0.

Означення 4. Під диз'юнктною сумою будемо розуміти домен з визначенням

[D₁+D₂+...+D_n]={ (d_i, i) | d_i Î D_i, 0<i<n+1 },

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

8.4. Формалізація семантики мови|язик| функціонального програмування SML|

SMalL

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

E1==E2 | E1+E2

2. С::= I=E | if (E) C1 else C2 |

while (E) C | C1;C2

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

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

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

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

8.4.2. Обчислювальна модель на основі станів програми мови SmalL

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

Параметр	Домен	Співвідношення
Стан	State	(s) State=Memory
Пам’ять	Memory	(m) Memory = Ide -> [Value+{unbound}]
Значення	Value	(v) Value=Int+Bool

8.5.1. Семантичні речення для виразів

E: Exp -> [State -> [[Value, State] + {error}]];

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

якщо v - значення E в s, s'- стан після означування;

E[E]s = error,

якщо виникає помилка невідповідності типів.

8.5.2. Семантичні речення для команд

С: Com -> [State -> [ State + {error}]].

8.5.3. Семантичні речення для денотатів:

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.

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