2. Денотаційна семантика.

Нехай задані

• область даних D, де визначені операції сигнатури Ω і елементарні предикати сигнатури П;

• множина імен R.

Множину всіх відображень В з множини R в область даних В позначимо через B= і будемо називати множиною станів пам’яті або інформаційним середовищем.

З даною програмою Р зв’яжемо часткову функцію : В → B, яка повинна обчислюватись цією програмою. Значення функції (b) на стані пам’яті b Є В будемо позначати через (b).

Визначимо:

а) семантику виразів: : : В → D, де у - вираз;

б) семантику імен виразів: : : В → R, де х - змінна;

в) семантику умов: : : В → {0,1}, де и - умова.

Виходячи з цього означення і абстрактного синтаксису, денотаційну семантику процедурних програм можна визначити так:

1. P = (x := y) (b)(r) = (b,r) = (if( (b) = r,

2. P = ( )) (b) = ( ;

3. P = if(u, (b) = (if( );

4. P = while(u,Q) (b) = (b)),

де n - найменше натуральне число такe, що для всіх 0 ≤ т < n мають місце умови Більш лаконічно цe можна записати у вигляді рекурсивного означення:

(b) = if( = 0, b, ).

3. Операційна семантика

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

Пару (Р,b), де Р - програма, a b - стан пам’яті, називатимемо станом обчислень. Серед станів обчислень виділимо стан (succ, b) для фіксації успішного завершення обчислень програмою, тобто стан (succ,b) є заключним станом обчислень.

Бінарне відношення переходів → на станах обчислень позначається через (P, b) → (Р', b') і знаходиться за такими правилами:

а) (x :=y,b) →(succ, );

;

в) , де

г) ;

д) ;

e) ;

є) .

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

(P,b) ( ) ( ) …

Ця історія може бути як скінченна, так і нескінченна. Якщо історія скінченна, то її останнім етапом є стан (sucс, b), а стан пам’яті b Є В називається результатом виконання програми Р.

Нехай відношення * означає рефлексивно-транзитивне замикання відношення переходів , тобто s * s' ⇔ 1)s = s' або 2)s s' або 3)s s" * s'.

При цьому кожний стан обчислень породжує єдину історію обчислень.

Тепер виникає питання, як пов’язані між собою денотаційна і операційна семантики? Відповідь на це питання дає таке твердження.

Теорема 3.1. (b) = b' ⇔ (P,b) * (succ, b').

Доведення виконується методом математичної індукції з розглядом можливих варіантів обчислення функції (b) (пункти 1) - 4)) і відношення * (пункти а) - g)).

Розглянемо приклад процедурної програми.

Програма обчислення найбільшого спільного дільника двох натуральних чисел (НСД).

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

1. НСД(х,х) = х;

2. х>у ⇒НСД(х, у) =НСД(х -у,у);

3. х < у ⇒ НСД(х, у) =НСД(х, у - х).

Імперативна програма має такий вигляд:

НСД(х ,у).

Вхід: х, у Є N.

Вихід: d Є N.

begin

а := х;

b := у;

while а ≠ b do

if а > b then а := а - b else b := b - a; fi;

od;

d := а;

end