Київський національний університет

імені Тараса Шевченка

Методичні рекомендації

до практичних занять

з курсу «Теорія програмування»

Київ – 2009

УДК 681.3

Рецензенти:

Бєлов Ю.А., доктор фізико-математичних наук, професор факультету кібернетики Київського національного університету імені Тараса Шевченка

Дорошенко А.Ю., доктор фізико-математичних наук, професор, заступник директора з наукової роботи Інституту програмних систем НАН України

Затверджено Вченою радою факультету кібернетики Протокол № __ від __ ______ 2010 р.

Нікітченко М.С., Панченко Т.В. Методичні рекомендації до практичних занять з курсу «Теорія програмування». – Київ, 2010. – ___ с.

Навчальний посібник призначений для студентів спеціальності інформатика, які проходять курс «Теорія програмування», або споріднений, в якому розглядаються питання синтаксису, семантики та коректності програм.

В посібнику надаються розв’язки задач, які виникають при розгляді зазначених питань, а також детальні коментарі та пояснення.

© Нікітченко М.С., Панченко Т.В., 2010.

Зміст

Вступ 4

1. Синтаксис та семантика. Мова SIPL. Композиційна семантика 4

1.1. Синтаксис мови SIPL 4

1.2. Композиційна семантика мови SIPL 6

1.2.1. Дані 6

1.2.2. Функції 8

1.2.3. Композиції 9

1.2.4. Програмні алгебри 10

1.3. Побудова семантичного терму програми 11

1.4. Доведення коректності програм 13

1.5. Розв’язки типових задач 14

1.6. Розширення мови SIPL: Введення булевих змінних 45

1.6.1. 45

1.7. Приклади розв’язків задач. 49

1.8. Розширення мови SIPL: Введення викликів функцій 54

1.9. Приклади задач 56

1.10. Завдання для самостійної роботи 59

1.11. Приклади завдань для контрольної роботи. 59

Тема 2. Формальні мови та граматики 61

2.1. Побудова мови за допомогою системи рівнянь з регулярними коефіцієнтами 61

2.2. Завдання для самостійної та контрольної роботи 68

2.3. Нормальні форми Хомського та Грейбах 68

2.4. Завдання для самостійної та контрольної роботи 80

Тема 3. Рекурсія та найменша нерухома точка. Неперервність операторів 81

Тема 4. Натуральна семантика 84

Тема 5. Аксіоматична семантика 93

Література 99

Вступ

Теорія програмування - …

Доведення коректності програм

…

семантика

аспекти програм

методи, способи …

побудова і доведення (+ за побудовою)

формалізація, математичні формальні підходи до: …

1. Синтаксис та семантика. Мова sipl. Композиційна семантика

1.1. Синтаксис мови sipl

Для побудови дерева синтаксичного виводу, композиційного семантичного терму і доведення коректності програми ми будемо використовувати мову SIPL. Говорячи неформально, мова SIPL має змінні цілого типу, над якими будуються арифметичні вирази та умови. Основними операторами є присвоєння, послідовне виконання, розгалуження, цикл.

Мова SIPL може розглядатися як надзвичайно спрощена традиційна мова програмування, наприклад, Паскаль. В мові SIPL відсутні типи, оператори вводу-виводу та багато інших конструкцій традиційних мов програмування. Разом з тим ця мова є досить потужною, щоб програмувати різні арифметичні функції, більше того, в цій мові можуть бути запрограмовані всі обчислювальні функції над цілими числами.

Для опису синтаксису мов зазвичай використовують БНФ – форми Бекуса-Наура. Програми або їх частини виводяться із метазмінних (нетерміналів), які записуються у кутових дужках. Метазмінні задають синтаксичні класи. В процесі виводу метазмінні замінюються на праві частини правил, що задають ці метазмінні. Праві частини для однієї метазмінної розділяються знаком альтернативи « | ». Процес породження припиняється, якщо всі метазмінні замінено на термінальні символи.

Синтаксис мови SIPL можна задати за допомогою наступної БНФ:

Таблиця 1.1

Ліва частина правила – метазмінна (дефінієндум)	Права частина правила (дефінієнс)	Ім’я правила
<програма> ::=	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 як набір речень (слів), які виводяться з метазмінної <програма>. Щоб переконатись у синтаксичній правильності програми треба побудувати її вивід, який можна подати у вигляді дерева.