Обчислення значень семантичних термів

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

Приклад 1.4 Обчислимо значення семантичного терму програми GCD на вхідному даному [M a8, N a16].

Процес обчислення значення задається формулами таблиці 1.5. Ці формули, як і формули таблиці 1.6, є загальними правилами обчислень. Щоб їх застосовувати, треба робити конкретизацію загальних правил подібно до того, як описано в прикладі 1.3. Отже, завдання полягає в отриманні значення наступної аплікації:

WH(S²(neq, MÞ, NÞ), IF(S²(gr, MÞ, NÞ),

AS^M( S²(sub, MÞ, NÞ)), AS^N( S²(sub, NÞ, MÞ)))) ([M a8, N a16]).

Правила для обчислення циклу AF_WH говорять про необхідність поступового обчислення станів st₀, st₁, …, та перевірки відповідних умов. Отримуємо уніфікацію

[fb/S²(neq, MÞ, NÞ),

f s/ IF(S²(gr, MÞ, NÞ)), AS^M( S²(sub, MÞ, NÞ), AS^N( S²(sub, NÞ, MÞ))),

st/[M a8, N a16], st ₀/[M a8, N a16]].

Переходимо до обчислення fb(st₀), яке конкретизується аплікацією

S²(neq, MÞ, NÞ)([Ma8, Na16]).

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

S²(neq, MÞ, NÞ)([Ma8, Na16])= neq(MÞ, NÞ)([Ma8, Na16])

=neq(MÞ([Ma8, Na16]), NÞ([Ma8, Na16])).

Застосовуючи правила обчислення функції розіменування, отримуємо, що S²(neq, MÞ, NÞ)([Ma8, Na16])= neq(8,16)=true.

Правила обчислення для циклу говорять про необхідність обчислення за правилом st₁=f s(st₀), що конкретизується наступним чином:

IF(S²(gr, MÞ, NÞ), AS^M( S²(sub, MÞ, NÞ)),

AS^N( S²(sub, NÞ, MÞ)))([Ma8, Na16]).

Обчислення цієї аплікації полягає в застосуванні правила AF_IF для обчислення умовного оператора. Спочатку обчислюємо умову

S²(gr, MÞ, NÞ))([Ma8, Na16])= gr(MÞ([Ma8, Na16]), NÞ([Ma8, Na16]))= gr(8, 16)= false.

При хибній умові за правилом AF_IF обчислюється AS^N( S²(sub, NÞ, MÞ))([Ma8, Na16]). Отримуємо за правилом AF_AS

AS^N( S²(sub, NÞ, MÞ))([Ma8, Na16])= [Ma8, Na16]Ñ[NaS²(sub, NÞ, MÞ)([Ma8, Na16])] =[Ma8, Na16]Ñ[Nasub(NÞ([Ma8, Na16]), MÞ([Ma8, Na16]))] =[Ma8, Na16]Ñ[Nasub(16,8)]=[Ma8, Na16]Ñ[Na8] = [Ma8, Na8].

Отже, st₁ конкретизується як [Ma8, Na8]. Тепер за правилом AF_WH обчислюємо умову циклу на отриманому стані:

S²(neq, MÞ, NÞ)([Ma8, Na8])= neq(8,8)= false.

Таким чином, остаточний стан є [Ma8, Na8] _▄

 

1.3.8 Загальна схема формалізації мови SIPL

 

Підсумуємо схему формалізації, яка була застосована для мови SIPL. Зазначимо, що в першому наближенні мова L задається як трійка виду (Synt, Sem, interpretation), де Synt – опис синтаксичного аспекту (опис текстів програм), Sem – опис семантичного аспекту (опис смислу програм), interpretation: Synt ® Sem  – інтерпретація програм, яка кожній програмі співставляє її смисл (значення). Інтерпретацію також називають денотацією.

Спочатку мали початковий опис мови (Synt ₀, Sem ₀, interpretation ₀), який складався з формального подання синтаксису Synt ₀ у вигляді БНФ та неформального опису семантики Sem ₀. Інтепретація interpretation ₀: Synt ₀ ® Sem ₀ також була неформальною.   

Для формалізації семантики було вибрано формалізм функціональних алгебр. Цей формалізм також можна трактувати як певну мову, синтаксис якої задається термами алгебри Synt ₁, семантика Sem ₁ – фунціями з носія алгебри, а інтерпретація interpretation ₁: Synt ₁ ® Sem ₁  є просто інтерпретацією термів в алгебрі.

Визначення формальної семантики надає можливість надати формальне визначення мови SIPL наступним чином:

· синтаксис Synt ₀ задається БНФ,

· семантика Sem ₁ задається функціями,

· інтерпретація interpretation_SIPL : Synt ₀ ® Sem ₁ є добутком відображень sem_P та interpretation ₁, тобто 

interpretation_SIPL = sem_P · interpretation ₁.

(Тут множення · тлумачиться як композиція довільних відображень.)

Таким чином, мова SIPL уточнються трійкою

(Synt ₀, Sem ₁, sem_P · interpretation ₁).

Правда, тут вважаємо, що відображення sem_P переводить програми з Prog  в терми, що задають функції з FS.

Кожен компонент цієї трійки визначений формально. Вказана формалізація наведена на малюнку 1.5.

 

 

---

Дата добавления: 2019-02-13; просмотров: 201; Мы поможем в написании вашей работы!

Поделиться с друзьями:

---

---

Мы поможем в написании ваших работ!