1.3 Формальний опис семантики мови sipl

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

Перейдемо до розгляду композиційної семантики мови SIPL.

1.3.1 Дані.

Базові типи даних – множини цілих чисел, бульових значень та змінних (імен):

Int={ . . . , -2, -1, 0, 1, 2, . . . }
Bool={true, false}
Var={X, Y, … }

Похідні типи – множина станів змінних (наборів іменованих значень, наборів змінних з їх значеннями):

State=Var Int

Приклади станів змінних: [M8, N16], [M3, X 4, Y2, N16].

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

Операції на множині Int. Символам +, – , ,  відповідають операції add, sub, mult, div (додавання, віднімання, множення, ділення). Це бінарні операції типу Int² Int.

Операції на множині Bool. Символам , ,  відповідають операції or, and, neg. Це бінарні операції типу Bool²  Bool (диз’юнкція та кон’юнкція) та унарна операція типу Bool Bool (заперечення).

В мові також є операції змішаного типу. Символам операцій порівняння <, , =, , , > відповідають операції less, leq, eq, neq, geq, gr. Це бінарні операції типу Int²  Bool.

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

Алгебра цілих чисел: A_Int=<Int; add, sub, mult, div >.

Алгебра бульових значень: A_Bool=<Bool; or, and, neg >.

Якщо додати операції порівняння, отримаємо двоосновну алгебру базових даних:

A_Int_Bool =<Int, Bool; add, sub, mult, div, or, and,

neg, less, leq, eq, neq, geq, gr >.

Для опису мови SIPL треба додати ще одну основу – множину станів змінних. На цій основі задана бінарна операція накладання  (для цієї операції іноді вживається термін накладка). Ця операція за двома станами будує новий стан змінних, до якого входять всі іменовані значення з другого стану, та ті значення з першого стану, імена яких не входять до першого стану. Ця операція подібна до операції копіювання каталогів з спеціальним випадком однакових імен файлів у двох каталогах. В цьому випадку файл з першого каталога замінюється файлом з тим же іменем з другого каталогу.

Наприклад:

[M8, N16]  [M3, X 4, Y2]= [M3, N16, X 4, Y2].

Введемо зразу і відношення розширення  станів новими іменованими значеннями. Наприклад,

[M8, N16]  [M8, X 4, Y2, N16].

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

Для створення та оперування із станами змінних треба визначити дві функції: іменування x: Int  State та розіменування x: State  Int, які мають параметр xVar:

x(n)=[xn]
x(st)=st(x)

Тут і в подальшому вважаємо, що nInt, stState. Перша функція іменує іменем x число n, створюючи стан [xn], друга бере значення імені x в стані st. Сама формула ґрунтується на тому факті, що стани змінних можуть тлумачитись як функції виду VarInt. Функція розіменування є частковою. Вона не визначена, якщо x не має значення в стані st.

Наприклад:

M(5)=[M5],
Y([M3, X4, Y2])=2,
Y([M3, X4]) не визначене.

Крім того, введемо

функцію-константу арифметичного типу : StateInt, таку що (st)=n,
функції-константи бульового типу , : StateBool такі, що (st)=true, (st)=false,
тотожну функцію id: StateState, таку, що id(st)=st.