Визначення семантичних термів
КИЇВСЬКИЙ НАЦІОНАЛЬНИЙ УНІВЕРСИТЕТ ІМЕНІ ТАРАСА ШЕВЧЕНКА
М.С. Нікітченко
ТЕОРЕТИЧНІ ОСНОВИ ПРОГРАМУВАННЯ
Навчальний посібник
Незавершений чорновий варіант посібника
Прохання не розповсюджувати
УДК 004.4
ББК 22.18я73
Н62
Рецензенти
д-р фіз.-мат. наук Ю.А. Бєлов,
д-р фіз.-мат. наук А.Ю. Дорошенко
Затверджено вченою радою факультету кібернетики
(протокол №5 від 17 січня 2007 року)
Нікітченко М.С.
Н62 Теоретичні основи програмування: Навчальний посібник. – Київ: Видавничо-поліграфічний центр "Київський університет", 2009. – ??? с.
Викладено теоретичні основи програмування. Матеріал подано в семантико-синтаксичному стилі на основі єдиного для програмування, математичної логіки та теорії алгоритмів композиційно-номінативного підходу. Викладення проілюстровано прикладами, у кінці розділів запропоновано питання для самоконтролю та вправи для самостійного розв’язання.
Для студентів спеціальностей “Інформатика”, “Прикладна математика“, “Системний аналіз”.
УДК 004.4
ББК 22.18я73
ã М.С.Нікітченко, 2009
© Київський національний університет імені Тараса Шевченка,
ВПЦ "Київський університет", 2009
ВСТУП. 6
1. Формалізація простої мови програмування. 19
1.1 Неформальний опис простої мови програмування. 19
1.2 Формальний опис синтаксису мови SIPL. 21
|
|
|
1.3 Формальний опис семантики мови SIPL. 28
1.4 Властивості програмної алгебри. 43
2. Розвиток основних понять програмування. 55
2.1 Аналіз словникових визначень поняття програми. 56
2.2 Розвиток поняття програми з гносеологічної точки зору 57
2.3 Розвиток основних понять програмування. 63
2.3.1 Початкова тріада понять програмування. 64
2.3.2 Тріада прагматичності програм.. 67
2.3.3 Тріада основних понять програмування. 68
2.3.4 Пентада основних понять програмування. 70
2.4 Розвиток основних програмних понять. 73
2.4.1 Тріада основних програмних понять. 73
2.4.2 Пентада основних програмних понять. 78
2.5 Сутнісні та семіотичні аспекти програм.. 81
2.6 Програми і мови. 84
2.7 Пентада програмних понять процесного типу. 85
3. Формалізація програмних понять. 89
3.1 Теоретико-функціональна формалізація. 89
3.2 Класи функцій. 90
3.3 Програмні системи. 91
3.4 Рівні конкретизації програмних систем.. 93
4. Синтактика: формальні мови та граматики. 97
4.1 Розвиток понять формальної мови та породжучої граматики 97
4.2 Визначення основних понять формальних мов. 107
Операції над формальними мовами. 109
4.3 Породжуючі граматики. 111
4.4 Приклад породжуючої граматики та її властивості Ошибка! Закладка не определена.
|
|
|
4.5 Ієрархія граматик Хомського. 116
4.6 Автоматні формалізми сприйняття мов. 121
4.6.1 Машини Тьюрінга. 122
4.6.2 Еквівалентність машин Тьюрінга та породжуючих граматик. 125
4.6.3 Лінійно-обмежені автомати. 128
4.6.4 Магазинні автомати. 129
4.6.5 Скінченні автомати. 130
4.7 Методи подання синтаксису мов програмування. 132
4.7.1 Нормальні форми Бекуса–Наура. 132
4.7.2 Модифіковані нормальні форми Бекуса–Наура. 133
4.7.3 Синтаксичні діаграми. 134
4.8 Властивості контекстно-вільних граматик. 137
4.8.1 Видалення несуттєвих символів. 137
4.8.2 Видалення e-правил. 140
4.8.3 Нормальна форма Хомського. 141
4.8.4 Нормальна форма Грейбах. 142
4.8.5 Рекурсивні нетермінали. 142
4.9 Властивості контекстно-вільних мов. 143
4.10 Операції над формальними мовами. 143
4.11 Дерева виводу. 146
4.12 Однозначні та неоднозначні граматики. 148
4.13 Розв’язні та нерозв’язні проблеми КВ-граматик та мов 149
4.14 Рівняння в алгебрах формальних мов. 150
5. Теорія рекурсії (теорія найменшої нерухомої точки) 158
5.1 Рекурсивні визначення та рекурсивні рівняння. 158
5.2 Частково впорядковані множини, границі ланцюгів та 
-області 160
5.3 Неперервні відображення. 161
5.4 Теореми про нерухомі точки. 162
5.5 Конструювання похідних -областей. 164
5.6 Властивості оператора найменшої нерухомої точки. 169
|
|
|
5.7 Застосування теорії ННТ. 170
5.7.1 Уточнення синтаксису мов програмування. 171
5.7.2 Семантика мов програмування. 174
5.7.3 Рекурсивні розширення мови SIPL. 178
6. Семантика. 187
6.1 Композиційна семантика. 187
6.2 Денотаційна семантика. 187
6.3 Функціональні системи Дж. Бекуса. 187
6.4 Аплікативна аксіоматична (операційна) семантика. 187
7. Програмні логіки. 204
7.1 Розвиток основних понять логіки. 204
7.1.1 Інтенсіональні аспекти понять математичної логіки. 205
7.1.2 Розвиток поняття даного. 211
7.1.3 Розвиток поняття функції 215
8. Натуральна семантика. 218
8.1 Натуральна семантика мови SIPL. 218
8.2 Аксіоматична методи верифікації програм.. 218
8.3 Аксіоматична система верифікації програм мови SIPL 218
9. Збагачення простої мови програмування (композиційно-номінативні мови) 237
10. Абстрактні типи даних. 238
11. Абстрактна обчислюваність в мовах програмування. 239
11.1 Постуляційні визначення повних класів обчислюваних функцій для даних абстрактного рівня. 240
11.2 Постуляційні визначення обчислюваних функцій над номінативними даними. 241
11.2.1 Функції над номінативними даними. 242
11.2.2 Композиції функцій над номінативними даними. 243
11.2.3 Обчислювані функції над номінативними даними. 244
|
|
|
11.3 Натуральна обчислюваність функцій. 246
12. Формальні методи специфікації та верифікації програм.. 252
Список літератури. 263
ВСТУП
Інформаційні технології застосовуються зараз практично у всіх сферах життя людства. Ці технології корінним чином змінили світ. Значні успіхи в телекомунікаціях, енергетиці, транспорті, медицині, освіті, космічних дослідженнях та інших сферах діяльності людства, досягнуто завдяки використанню інформаційних технологій. Однак таке розширення області їх застосувань має і негативну сторону. Людство стає все більш залежним від надійного і правильного функціонування комп’ютерних систем; помилки в їх роботі часом ведуть до величезних фінансових, а навіть і людських втрат. Дотепер фірми-розробники програмного забезпечення не дають гарантію на програмні продукти, що вони пропонують користувачу. Але такого фактично немає ні в одній іншій області діяльності. Будь-який легальний продавець якогось товару дає гарантії якості і готовий нести (пригадаємо повернення мільйонів автомобілів на заводи виробника у разі виявлення дефектів) фінансову і юридичну відповідальність за поставку недоброякісного продукту.
Можна привести і безліч інших прикладів, коли погане програмне забезпечення приводило до знищення космічних ракет, аварій на заводах, гідроелектростанціях, і т.п. Про складний стан справ говорять і самі фахівці в області комп'ютерних технологій. У чому ж причини? Вони, безумовно, різноманітні і зачіпають наукові, економічні, соціальні, психологічні і інші проблеми створення і використання інформаційних технологій. Серед наукових однією з найважливіших є проблема створення ефективних методів розробки програмних систем. Такі методи мають базуватися на розвиненій теорії програмування, яка має на меті дослідження програм та методів їх аналізу і синтезу. Відзначимо, що тут термін програма тлумачиться у широкому смислі, охоплюючи, зокрема, як програми конкретних мов програмування, так і програмні системи.
Даний посібник може розглядатися як вступ у теорію програмування. Ця дисципліна є базовою нормативною дисципліною спеціальності "Інформатика".
Щоб надати початкове уявлення про цю дисципліну треба визначити її мету і завдання, об’єкт та предмет, а також вказати на її основні методи.
Метою і завданням навчальної дисципліни "Теорія програмування" є засвоєння основних концепцій, принципів та понять сучасного, зокрема композиційного, програмування. У світоглядному аспекті, поняття і методи теорії програмування необхідні для обгрунтування та формалізації способів розробки правильних та ефективних програм. В прикладному аспекті, апарат теорії програмування необхідний для адекватного моделювання мов специфікацій і програмування та використання побудованих моделей для створення сучасних програмних та інформаційних систем високої якості.
Об’єктом навчальної дисципліни "Теорія програмування" є програми, а її предмет включає в себе вивчення основних (базових) понять теорії програмування, розгляд основних аспектів програм (семантика та синтаксис), їх формалізацію та дослідження, а також уточнення основних методов розробки програм.
Вимоги до знань та вмінь. Для засвоєння матеріалу необхідні знання основ елементарної математики, дискретної математики, алгебри, математичної логіки та теорії алгоритмів. Відповідно в курсі будуть використовуватись методи теорії множин, дискретної математики, універсальної алгебри, математичної логіки та теорії алгоритмів.
Місце в структурно-логічній схемі спеціальності. Нормативна навчальна дисципліна "Теорія програмування" є складовою циклу професійної підготовки фахівців освітньо-кваліфікаційного рівня "бакалавр". Курс теорії програмування потрібен для подальшого вивчення нормативних дисциплін "Системне програмування", "Бази даних та інформаційні системи", "Інтелектуальні системи", "Теорія обчислень", "Штучний інтелект", "Формальні методи розробки програмних систем", "Інформаційні технології", "Прикладна логіка", низки спецкурсів відповідного напряму.
Структура курсу:
- Основні програмні поняття
- Синтактика
- Семантика
- Методи розробки програм
Для подання інтенсіональних аспектів будемо використовувати принципи, постулати та аксіоми. Принципи найбільш загальні, постулати більш конкретні і більш чіткіші, аксіоми більш формальні. Тобто є послідовність термінів із зменшеням загальності та невизначеності: принцип, постулат, аксіома.
Назва курсу «Теорія програмування» складається з двох термінів – «теорія» та «програмування». Перш ніж переходити до розгляду «теорії програмування», розглянемо основні властивості кожного із термінів, які складають назву курсу.
1. Формалізація простої мови програмування
Центральним завданням теорії, зокрема і теорії програмування, є визначення та дослідження її основних понять. Зробити це не так просто, бо в теоріях, як правило, використовується багато понять, які пов’язані одне з одним. Тому спочатку доцільно ввести основні поняття теорії програмування на невеликому прикладі. Це буде програма знаходження найбільшого спільного дільника двох чисел. Програма записана на деякій простій мові. В цьому розділі ця мова буде формалізована, тобто буде описано її синтаксис та семантику. Також будуть досліджені деякі властивості програм цієї мови.
1.1 Неформальний опис простої мови програмування
Для посилання на певну мову треба надати їй ім’я. Для імені часто використовують абревіатуру короткої характеристики мови. Зважаючи на традиції використання латинських літер в науковій символиці, утворимо абревіатуру SIPL від характеристики SImple Programming Language (Проста Мова Програмування).
Цю абревіатуру можна розшифрувати трохи інакше, вказуючи на імперативність або структурованість цієї мови:
Simple Imperative Programming Language
Structured Imperative Programming Language
Говорячи неформально, мова SIPL має змінні цілого типу, над якими будуються арифметичні вирази та умови. Основними операторами є присвоєння, послідовне виконання, розгалуження, цикл.
Мова SIPL може розглядатися як надзвичайно спрощена традиційна мова програмування, наприклад, Паскаль. В мові SIPL відсутні типи, оператори вводу-виводу та багато інших конструкцій традиційних мов програмування. Разом з тим ця мова є досить потужною, щоб програмувати різні арифметичні функції, більше того, в цій мові можуть бути запрограмовані всі обчислювальні функції над цілими числами.
Приклад 1.1. Програма GCD знаходження найбільшого спільного дільника чисел M та N за алгоритмом Евкліда:
GCD º
Begin
while M¹N do
if M>N then M:=M–N else N:=N–M
End
Оскільки програми призначені для обчислення результатів за вхідними даними, розглянемо неформально процес виконання цієї програми на вхідних даних, у яких M має значення 8, а N – 16. Вважаємо, що дані записуються в пам’ять, а оператори виконуються деяким процесором. Тому розмітимо програму, відмічаючи оператори мітками:
0: begin
1: while M¹N do
2: if M>N then 3: M:=M–N else 4: N:=N–M
End
Процес виконання програми можна подати у вигляді таблиці, кожний рядок якої вказує на номер виконуваного оператора та на нові значення змінних (детали процесу виконання можна знайти з книжках з основ програмування). Для нашого прикладу така таблиця може мати наступний вигляд.
Таблиця 1.1
| Мітка | Значення умови | Значення M | Значення N |
| 0 | 8 | 16 | |
| 1 | M¹N – true | ||
| 2 | M>N – false | ||
| 4 | 8 | ||
| 1 | M¹N – false |
Програма припиняє роботу із значеннями M та N, рівними 8. Це число і є найбільшим спільним дільником.
Аналізуючи цю програму та процес її виконання, відзначаємо два аспекти:
· синтаксичний (текст програми),
· семантичний (смисл програми – те, що вона робить).
В нашому прикладі ні синтаксис, ні семантика не задані точно (формально). Ми маємо лише інтуїтивне розуміння програм мови SIPL. Тому важко відповідати на питання, які вимагають точного опису мови. Наприклад незрозуміло, чи можна поставити крапку з комою між оператором та символом end, що дозволяється робити в багатьох мовах програмування (синтаксичний аспект). Незрозуміло також, чи завжди наведена програма буде обчислювати найбільший спільник дільник для довільних значень M та N (семантичний аспект).
Щоб відповідь на такі питання стала можливою, необхідно надати строге (формальне) визначення нашої мови програмування. Лише тоді можна буде застосувати математичні методи дослідження програм та будувати відповідні системи програмування, зокрема транслятори та інтерпретатори.
Безумовно, уточнення (експлікацію) синтаксичного та семантичного аспектів можна давати по-різному. Ми спочатку розглянемо традиційні формалізми для опису мов.
1.2 Формальний опис синтаксису мови SIPL
Для опису синтаксису мов зазвичай використовують БНФ (Форми Бекуса-Наура). Програми (або їх частини) виводяться із метазмінних (нетерміналів), які записуються у кутових дужках. Метазмінні задають синтаксичні класи. В процесі виводу метазмінні замінюються на праві частини правил, що задають ці метазмінні. Праві частини для однієї метазмінної розділяються знаком альтернативи « | ». Процес породження припиняється, якщо всі метазмінні замінено на термінальні символи.
Синтаксис мови SIPL можна задати за допомогою наступної БНФ:
Таблиця 1.2
| Ліва частина правила – метазмінна (дефінієндум) | Права частина правила (дефінієнс) | Ім’я правила |
| <програма> ::= | begin <оператор> end | NP1 |
| <оператор> ::= | <змінна>:=<вираз> | <оператор> ; <оператор>| if <умова> then <оператор> else <оператор> | while <умова> do <оператор> | begin <оператор> end | skip | NS1 NS2 NS3 NS4 NS5 NS6 |
| <вираз> ::= | <число> | <змінна> | <вираз> + <вираз> | <вираз> – <вираз> | <вираз> * <вираз> | <вираз> ÷ <вираз> | (<вираз>) | NA1– NA7 |
| <умова> ::= | true | false | <вираз> < <вираз> | <вираз> £ <вираз> | <вираз> = <вираз> | <вираз> ¹ <вираз> | <вираз> > <вираз> | <вираз> ³ <вираз> | <умова> Ú <умова> | <умова> Ù <умова> | Ø <умова> | (<умова>) | NB1– – NB12 |
| <змінна> ::= | M | N | . . . | NV1–… |
| <число> ::= | . . . –1 | 0 | 1 | 2 | 3 | . . . | NN1–… |
Наведена БНФ задає мову SIPL як набір речень (слів), які виводяться з метазмінної <програма>. Точне визначення виводу буде подано пізніше, зараз тільки відмітимо, що вивід можна подати у вигляді дерева.
Щоб переконатись у синтаксичній правильності програми треба побудувати її вивід. Зокрема, для нашої програми GCD маємо наступне дерево виводу.
Малюнок 1.1. Дерево синтаксичного виводу програми GCD
Побудоване дерево синтаксичного виводу дозволяє стверджувати синтаксичну правильність програми GCD. Дійсно, якщо записати зліва направо послідовність усіх термінальних символів, то отримаємо програму GCD, що говорить про її вивідність у БНФ мови SIPL, тобто про її синтаксичну правильність.
Аналізуючи далі наведену БНФ можна відзначити, що вона досить просто описує основні конструкції мови SIPL. Але зворотною стороної цієї простоти є неодзначність цієї БНФ. Наприклад, вираз X+Y*Z має два різних дерева виводу, що ведуть до різних семантик (малюнок 1.2). Тому неоднозначність БНФ значно ускладнює семантичний аналіз програм.
Малюнок 1.2. Дерева синтаксичного виводу виразу X+Y*Z
Однозначності побудови дерева синтаксичного виводу можна досягти введенням пріоритетів операцій та правил асоціативності для операцій одного пріоритету. Слід відзначити, що в математиці при описі пріоритетів, як правило, не розрізняють синтаксичний і семантичний аспекти, тому часто говорять, що пріоритети задають порядок виконання операцій (семантичний аспект), замість того, щоб говорити про порядок структурного аналізу виразу (синтаксичний аспект). Такий розгляд об’єкту, коли не виокремлюються його різні аспекти та складові, часто називають синкретичним. У випадку мови SIPL однозначність аналізу може порушуватись при формуванні операндів операцій (синтаксичних конструкторів) різного типу. Будемо виокремлювати три типи операцій:
· арифметичні (бінарні операції +, –, *, ¸) ,
· бульові (бінарні операції порівняння <, £, =, ¹, ³, >, бінарні операції диз’юнкції Ú та кон’юнкції Ù та унарна операція заперечення Ø),
· операторні (присвоєння, оператори послідовного виконання « _;_ », умовний оператор if_then_else_ та оператор циклу while_do_).
Тут символ підкреслення позначає операнд (або параметр) оператора. Перші дві групи операцій є традиційними, як і їх пріоритети. Третя група потребує певного пояснення. Справа в тому, що наприклад, синтаксична конструкція виду if b then S 1 else S 2; S 3 може аналізуватись по-різному. Одне трактування може відносити до умовного оператора (його else-частини) послідовність операторів S 2; S 3, інше трактування – тільки один оператор S 2. Різні трактування будуть задавати різну семантику. Те саме стосується і конструкцій виду while b do S 1; S 2 та S 1; S 2; S 3. На семантику також впливає порядок застосування операцій одного типу. Так, вираз a 1–a 2–a 3 можна аналізувати зліва-направо (лівоасоціативно), що можна подати як (a 1–a 2)–a 3, так і справа-наліво (правоасоціативно), що можна подати як a 1–(a 2–a 3) (=(a 1–a 2)+a 3). Щоб подолати неоднозначність синтаксичного аналізу будемо вважати, що всі бінарні операції лівоасоціативні (обчислюються зліва-направо) та що пріоритет операцій наступний (у порядку зменшення):
1) множення * та ділення ¸,
2) додавання + та віднімання –,
3) операції порівняння <, £, =, ¹, ³, >,
4) заперечення Ø,
5) кон’юнкція Ù,
6) диз’юнкція Ú,
7) умовний оператор if_then_else_ та оператор циклу while_do_,
8) послідовне виконання « ; » .
Зауважимо ще раз, що однозначність синтаксичного аналізу не зовсім адекватно подається пріоритетами операцій, які мають семантичну природу. Тому можливі розбіжності між цими поняттями.
Є і друга можливість досягти однозначності БНФ мови SIPL – ввести нові метасимволи та нові правила їх визначення. Пропонуємо читачам зробити це самостійно.
Наведені вище позначення метазмінних не зовсім зручні, тому часто використовують форми більш близькі до математики. А саме, введемо позначення для всіх синтаксичних категорій та нові метазмінні, що вказують на представників цих категорій.
Таблиця 1.3
| Метазмінна | Синтаксична категорія | Нова метазмінна |
| <програма> | Prog | P |
| <оператор> | Stm | S |
| <вираз> | Aexp | a |
| <умова> | Bexp | b |
| <змінна> | Var | x |
| <число> | Num | n |
В наведених позначеннях БНФ мови SIPL набуває наступного вигляду:
Таблиця 1.4
| Ліва частина правила – метазмінна | Права частина правила | Ім’я правила |
| P::= | begin S end | P1 |
| S::= | x:=a | S1 ; S2| if b then S1 else S2 | while b do S | begin S end | skip | S1–S6 |
| a::= | n | x | a1 + a2 | a1 – a2 | a1 * a2 | a1 ÷ a2 | (a) | A1– A7 |
| b::= | true | false | a1<a2 | a1£ a2 | a1= a2 | a1¹a2 | a1>a2 | a1³ a2 | b1Úb2 | b1Ù b2 | Øb | (b) | B1 – B12 |
| x::= | M | N | . . . | NV1–… |
| n::= | . . . –1 | 0 | 1 | 2 | 3 | . . . | NN1–… |
Надалі будемо користуватися введеними позначеннями для запису структури програм та їх складових.
Дотепер ми користувались інтуїтивним розумінням БНФ. Разом з тим слід розуміти, що можуть існувати різні уточнення БНФ (про це буде мова в розділі з синтактики). Зараз приймемо, що БНФ дозволяє прописати індуктивне визначення синтаксичних категорій. Дійсно, наведена БНФ визначає шість синтаксичних категорій (класів): Num, Var, Aexp, Bexp, Stm, Prog. Вони можуть бути задані наступним індуктивним визначенням.
1. База індукції:
· Num={…, -1, 0, 1, 2, 3, …},
· Var={X, Y, …},
· якщо nÎNum, то nÎAexp,
· якщо xÎVar, то xÎAexp,
· true, false належать Bexp,
· skip належить Stm.
2. Крок індукції:
· якщо a, a1, a2ÎAexp, то записи (вирази)
– a1 + a2,
– a1 – a2,
– a1 * a2,
– a1 ÷ a2,
– (a)
належать Aexp,
· якщо a1, a2ÎAexp, b , b1, b2ÎBexp, то записи (умови)
– a1<a2,
– a1£a2,
– a1=a2,
– a1¹a2,
– a1>a2,
– a1³a2,
– b1Úb2,
– b1Ùb2,
– Øb,
– (b)
належать Bexp,
· якщо xÎVar, aÎAexp, bÎBexp, S, S1, S2ÎStm, то записи (оператори)
– x:=a,
– S1 ; S2,
– if b then S1 else S2,
– while b do S,
– begin S end
належать Stm,
· якщо SÎStm, то запис begin S end належить Prog.
На підставі такого індуктивного визначення може бути задане визначення синтаксичних категорій за допомогою рекурентних співвідношень. Пропонуємо читачам зробити це самостійно.
Таким чином, можна стверджувати, що наведеними визначеннями синтаксис мови SIPL задато точно (формально).
Перейдемо тепер до визначення семантики мови SIPL.
1.3 Формальний опис семантики мови SIPL
Семантика задає значення (смисл) програми. Наш приклад показує, що смисл програми – перетворення вхідних даних у вихідні. В математиці такі перетворення називають функціями. Тому до семантичних понять відносять поняття даних, функцій та методів їх конструювання. Такі методи називаються композиціями, а відповідна семантика часто називається композиційною. Будемо вживати термін композиційна семантика, тому що саме композиції і визначають її властивості. Композиційна семантика є певною конкретизацією функціональної семантики, бо базується на тлумаченні програм як функцій.
Перейдемо до розгляду композиційної семантики мови SIPL.
Дані.
Базові типи даних – множини цілих чисел, бульових значень та змінних (імен):
· Int={ . . . , -2, -1, 0, 1, 2, . . . }
· Bool={true, false}
· Var={X, Y, … }
Похідні типи – множина станів змінних (наборів іменованих значень, наборів змінних з їх значеннями):
· State=Var ®Int
Приклади станів змінних: [Ma8, Na16], [Ma3, Xa 4, Ya2, Na16].
Операції на базових типах даних. Щоб відрізнити операції від символів, якими вони позначаються, будемо записувати їх жирним шрифтом, або писати спеціальні позначення. Ми тут оберемо другий варіант, вводячи нові позначення для операцій на типах даних.
Операції на множині Int. Символам +, – , *, ¸ відповідають операції add, sub, mult, div (додавання, віднімання, множення, ділення). Це бінарні операції типу Int2 ®Int.
Операції на множині Bool. Символам Ú, Ù, Ø відповідають операції or, and, neg. Це бінарні операції типу Bool2 ® Bool (диз’юнкція та кон’юнкція) та унарна операція типу Bool ® Bool (заперечення).
В мові також є операції змішаного типу. Символам операцій порівняння <, £, =, ¹, ³, > відповідають операції less, leq, eq, neq, geq, gr. Це бінарні операції типу Int2 ® 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 треба додати ще одну основу – множину станів змінних. На цій основі задана бінарна операція накладання Ñ (для цієї операції іноді вживається термін накладка). Ця операція за двома станами будує новий стан змінних, до якого входять всі іменовані значення з другого стану, та ті значення з першого стану, імена яких не входять до першого стану. Ця операція подібна до операції копіювання каталогів з спеціальним випадком однакових імен файлів у двох каталогах. В цьому випадку файл з першого каталога замінюється файлом з тим же іменем з другого каталогу.
Наприклад:
[Ma8, Na16] Ñ [Ma3, Xa 4, Ya2]= [Ma3, Na16, Xa 4, Ya2].
Введемо зразу і відношення розширення Í станів новими іменованими значеннями. Наприклад,
[Ma8, Na16] Í [Ma8, Xa 4, Ya2, Na16].
Це відношення не включаємо в алгебри, пов’язані з мовою SIPL, бо воно в цій мові безпосередньо не використовується, але буде корисним для доведення властивостей програм цієї мови.
Для створення та оперування із станами змінних треба визначити дві функції: іменування Þx: Int ® State та розіменування xÞ: State ® Int, які мають параметр xÎVar:
· Þx(n)=[xan]
· xÞ(st)=st(x)
Тут і в подальшому вважаємо, що nÎInt, stÎState. Перша функція іменує іменем x число n, створюючи стан [xan], друга бере значення імені x в стані st. Сама формула ґрунтується на тому факті, що стани змінних можуть тлумачитись як функції виду Var®Int. Функція розіменування є частковою. Вона не визначена, якщо x не має значення в стані st.
Наприклад:
· ÞM(5)=[Ma5],
· YÞ([Ma3, Xa4, Ya2])=2,
· YÞ([Ma3, Xa4]) не визначене.
Крім того, введемо
· функцію-константу арифметичного типу 
: State®Int, таку що (st)=n,
· функції-константи бульового типу 
, 
: State®Bool такі, що (st)=true, (st)=false,
· тотожну функцію id: State®State, таку, що id(st)=st.
Отримали багатоосновну алгебру даних мови SIPL
A_Int_Bool_State =<Int, Bool, State; add, sub, mult, div, or , and, neg,
less , leq, eq, neq, geq, gr, Þ x, xÞ, , id, Ñ, , >,
яка подана на наступному малюнку.
Малюнок 1.3. Алгебра даних мови SIPL
Зауваження 1.3 Є ще одна основа – Var. Але ніяких операцій на цій основі у мові SIPL не задано, тому зараз цю основу до алгебри даних не включаємо, але імена з Var використовуємо як параметри операцій іменування та розіменування.
Функції
Аналіз алгебри даних показує, що в мові SIPL можна вирізнити два види функцій: 1) n-арні функції на базових типах даних, та 2) функції над станами змінних. Другий вид функцій будемо називати номінативними функціями. Назва пояснюється тим, що вони задані на наборах іменованих даних (латинське nomen – ім’я).
Визначимо тепер наступні класи функцій, які будуть задіяні при визначенні семантики мови SIPL:
1. n-арні операції над базовими типами:
· FNA=Intn ® Int – n-арні арифметичні функції (операції),
· FNB=Booln ® Bool – n-арні бульові функції (операції),
· FNAB=Intn ® Bool – n-арні функції (операції) порівняння.
2. Функції над станами змінних
· FA=State ® Int – номінативні арифметичні функції,
· FB=State ® Bool – номінативні предикати,
· FS=State ® State – біномінативні функції –перетворювачі (трансформатори) станів.
Для операцій мови SIPL зазвичай n=2, а для бульової операції заперечення n=1.
Композиції
Нагадаємо, що композиції формалізують методи побудови програм. Аналіз мови SIPL дає підстави говорити про те, що будуть вживатися композиції різних типів, а саме:
· композиції, які пов’язані з номінативними функціями та предикатами,
· композиції, пов’язані з біномінативними функціями.
Перший клас композицій використовується для побудови семантики арифметичних виразів та умов, другий – операторів.
Цей клас композицій складається з композицій суперпозиції в n-арні функції, які задані на різних основах (класах функцій):
· суперпозиція номінативних арифметичних функцій в n-арну арифметичну функцію має тип Sn: FNA´FAn®FA,
· суперпозиція номінативних арифметичних функцій в n-арну фунцію порівняння має тип Sn: FNAB´FAn®FB,
· суперпозиція номінативних предикатів в n-арну бульову фунцію має тип Sn: FNB´FBn®FB.
Зауваження 1.4 Суперпозиції різного типу позначаємо одним знаком.
Суперпозиція задається формулою (тут f – n-арна функція, g1,…,gn – номінативні функції відповідного типу):
(Sn(f, g1,…,gn ))(st)=f(g1(st),…,gn(st)).
Другий клас композицій складається з наступних композицій.
· Присвоєння ASx: FA ® FS (x – параметр).
Присвоєння задається формулою:
ASx (fa)(st)=st Ñ[xa fa(st)]
· Послідовне виконання · : FS2®FS
Послідовне виконання задається формулою:
(f s 1·f s 2)(st)=f s 2(f s 1(st))
· Умовний оператор (розгалуження): IF:FB´FS2®FS. Задається формулою:
· Цикл (ітерація з передумовою): WH:FB´FS®FS. Задається рекурентно (індуктивно) наступним чином:
WH(fb,f s)(st)=stn, де
st0=st, st1=f s(st0), st2=f s(st1),…, stn=f s(stn-1), причому
fb(st0)=true, fb(st1)=true,…, fb(stn-1)=true, fb(stn)=false.
Важливо відзначити, що для циклу наведена послідовність визначається однозначно. Позначимо число n (кількість ітерацій циклу) як NumItWH((fb, fs), st). Однозначність визначення n дозволяє розглядати NumItWH((fb, fs), st) як тернарне відображення, яке залежить від fb, fs, st. Якщо цикл не завершується, то NumItWH((fb, fs), st) вважається невизначеним. Це відображення буде використовуватись в індуктивних доведеннях властивостей циклу.
Програмні алгебри
Побудовані композиції дозволяють стверджувати, що отримано алгебру функцій (програмну алгебру)
A_Prog =<FNA, FNB, FNAB, FA, FB, FS; Sn, ASx, ·, IF, WH, xÞ, id >.
Функції іменування Þx та накладання Ñ не включені в перелік операцій цієї алгебри, тому що композиції присвоєння та послідовного виконання замінюють їх. Разом з тим в перелік композицій включено функції (нуль-арні композиції) розіменування та тотожна функція. Це пояснюється тим, що вказані нуль-арні композиції мають не предметну (специфічну) природу, а логічну (загальнузначущу) природу, що дозволяє розглядати їх саме як загальні композиції (нехай і нуль-арні), а не як специфічні функції. Втім, цей розподіл є досить умовним.
|
|
Малюнок 1.4. Алгебра функцій (програмна алгебра)
Наведена алгебра містить багато «зайвих» функцій, які не можуть бути породжені в мові SIPL. Аналіз мови дозволяє стверджувати (цей факт буде доведено пізніше в теоремі 1.1), що функції, які задаються мовою SIPL, породжуються в алгебрі A_Prog з наступних базових функцій:
· add , sub, mult, div ÎFNA,
· or , and, neg ÎFNB,
· less , leq, eq, neq, geq, gr ÎFNAB,
· 
ÎFA (nÎInt),
· , ÎFB,
Підалгебру алгебри A_Prog, породжену наведеними базовими функціями, назвемо функціональною алгеброю мови SIPL і позначимо A_SIPL.
Зауважимо, що всі функції алгебри A_SIPL є однозначними (детермінованими) функціями. Це випливає з того, що всі базові функції є однозначними, а композиції зберігають цю властивість. (Довести цю властивість самостійно).
Формули для обчислення композицій та функцій алгебри A_Prog подамо у наступній таблиці (тут f – n-арна функція, fa, g1,…, gn – номінативні арифметичні функції, fb – номінативний предикат, f s, f s 1, f s 2 – біномінативні функції, st – стан, n – число).
Таблиця 1.5
| Композиція (функція) | Формула обчислення | Ім’я формули |
| Суперпозиція | (Sn(f, g1,…, gn))( st)=f(g1(st),…, gn(st)) | AF_S |
| Присвоєння | ASx (fa)(st)=st Ñ[xa fa(st)] | AF_AS |
| Послідовне виконання | f s 1·f s 2(st)=f s 2(f s 1(st)) | AF_SEQ |
| Умовний оператор | 
| AF_IF |
| Цикл | WH(fb,f s)(st)=stn, де st0=st, st1=f s(st0), st2=f s(st1), …, stn=f s(stn-1), причому fb(st0)=true, fb(st1)=true,…, fb(stn-1)=true, fb(stn)=false. | AF_WH |
| Функція розіменування | xÞ(st)=st(x) | AF_DNM |
| Тотожна функція | id(st)=st | AF_ID |
Зауваження 1.5 Наведені формули слід тлумачити з урахуванням частковості функцій. А саме, якщо значення однієї з функцій, що фігурує у формулі, не є визначенним, то і результат не буде визначенним. Так, для формули f s 1·f s 2(st)=f s 2(f s 1(st)) вважаємо, що коли f s 1(st) або f s 2(f s 1(st)) не визначені, то і результат не є визначеним.
Для роботи з частковими функціями використовують наступні позначення:
· f s(st) – значення f s на st не визначене,
· f s(st)¯ – значення f s на st визначене,
· f s(st)¯=r –значення f s на st визначене і дорівнює r.
З урахуванням частковості, формулу для послідовного виконання можна записати у наступному вигляді:
f s 1·f s 2(st)= 
Формула для умовного оператора буде мати вигляд
Інші формули можуть бути переписані аналогічним чином.
Зазначимо, что наведений вигляд формули зберігають і у випадку багатозначних (недетермінованих) функцій. Правда, тут такі функції розглядати не будемо▄
Побудована алгебра A_SIPL дозволяє тепер формалізувати семантику програм мови SIPL, задаючи їх функціональними виразами (семантичними термами) алгебри A_SIPL.
Визначення семантичних термів
Дотепер ми не дуже чітко розрізняли функціональний вираз алгебри A_Prog та функцію, що задається цим виразом. Наприклад, запис (f·g)·h можна тлумачити як функцію, і тоді її можна застосувати до стану st, та як вираз, і тоді, наприклад, вивчати тотожність (f·g)·h=f·(g·h). В математичній логіці таке розрізнення роблять явним, вважаючи, що (f·g)·h є виразом (термом, формулою), а не функцією. Саму ж функцію, яка задається цим виразом, позначають, наприклад, (f·g)·h I , де I – інтерпретація символів f, g, h в алгебрі A_Prog.
Таке розрізнення можна було б зробити і для мови SIPL. В такому випадку для опису (дескрипції) функцій, які задаються програмами мови SIPL, можуть використовуватись функціональні вирази алгебри A_SIPL, які називаються термами цієї алгебри. Такі класи термів будуються індуктивно, аналогічно класам синтаксичних категорій. Терми програмної алгебри будемо також називати семантичними термами. Але зараз не будемо використовувати різні позначення для термів та функцій, сподіваючись, що читач із контекста зрозуміє, про яке поняття іде мова. Разом з тим, слід пам’ятати, що це розрізнення є важливим в теорії програмування, яка чітко виокремлює синтаксис та семантику програм.
Дата добавления: 2019-02-13; просмотров: 321; Мы поможем в написании вашей работы! |
Мы поможем в написании ваших работ!