Криволап Андрій Володимирович. Побудова та дослідження програмних логік

brief description

Криволап Андрій Володимирович. Назва дисертаційної роботи: "Побудова та дослідження програмних логік"

Київський національний університет імені Тараса Шевченка
На правах рукопису
Криволап Андрій Володимирович
УДК 004.42
ПОБУДОВА ТА ДОСЛІДЖЕННЯ ПРОГРАМНИХ ЛОГІК
01.05.01 – теоретичні основи інформатики та кібернетики
Дисертація на здобуття наукового ступеня
кандидата фізико-математичних наук
Науковий керівник:
Нікітченко Микола Степанович
доктор фіз.-мат. наук, професор
Київ – 2016
2
ЗМІСТ
ПЕРЕЛІК УМОВНИХ ПОЗНАЧЕНЬ ТА СКОРОЧЕНЬ…………………………….4
ВСТУП…………………………………………………………………………………..5
РОЗДІЛ 1. Розширення логіки Флойда-Хоара………………………………………10
Висновки.....................................................................................................................18
РОЗДІЛ 2. Композиційно-номінативні моделі програм……………………………21
2.1. Номінативні множини……..…………………………………………………..21
2.2. Програмні алгебри………........................……………………………………..22
2.3. Монотонність та неперервність композицій…………..……………………..26
2.4. Властивості композиції побудови умови за прообразом…………….....…..32
2.5. Мова програмних логік для простих номінативних даних………………..35
2.6. Програмна логіка композиційно-номінативного типу для складних
ієрархічних даних......................................................................................................38
Висновки.....................................................................................................................47
РОЗДІЛ 3. Аксіоматичні системи Флойда-Хоарівскього типу для
часткових предикатів....................................................................................................49
3.1. Аксіоматична система логіки Флойда-Хоара для тотальних предикатів.....49
3.2. Аксіоматична система з доданими обмеженнями...........................................51
3.3. Аксіоматичні системи з T-зростаючими та F-спадними асерціями............61
3.4. Аксіоматичні системи з T- та F-обмеженнями................................................74
3.5. Аксіоматичні системи для композиційно-номінативних програмних
логік над ієрархічними даними...............................................................................87
Висновки...................................................................................................................103
РОЗДІЛ 4. Багатосортні аксіоматичні системи........................................................105
4.1. Багатосортна композиційно-номінативна програмна алгебра.....................105
4.2. Мова багатосортної композиційно-номінативної програмної логіки.........110
4.3. Аксіоматичні системи для багатосортної композиційно-номінативної
програмної логіки....................................................................................................113
Висновки...................................................................................................................119
3
ВИСНОВКИ.................................................................................................................121
СПИСОК ВИКОРИСТАНИХ ДЖЕРЕЛ....................................................................123
4
ПЕРЕЛІК УМОВНИХ ПОЗНАЧЕНЬ ТА СКОРОЧЕНЬ
t
тотальне відображення
p
часткове відображення
n
відображення зі скінченним графіком
f d( ) 
відображення
f
не визначено на даному
d
f d( ) 
відображення
f
визначено на даному
d
f d a ( ) 
відображення
f
визначено на даному
d
та рівне
a
f A[ ]
повний образ множини
A
за відображенням
f
1
f A[ ] 
повний прообраз множини
A
за відображенням
f
узагальнена рівність
T
булеве значення істини
F
булеве значення хиби

операція накладання

n
відношення належності номінативній множині

порожня множина
T
p
область істинності предиката
p
F
p
область хибності предиката
p
p

область невизначеності предиката
p
i
i
f
границя ланцюга
i
f
| відношення вивідності
|
відношення істинності
|
T
відношення логічного наслідку за істиною
|
F
відношення логічного наслідку за хибою
5
ВСТУП
Актуальність теми дослідження. Проблема специфікації та автоматизації
доведення коректності програмних систем є складною, але важливою для
побудови надійного програмного забезпечення. Для підвищення надійності таких
систем були створені різні методи їх розробки, зокрема, і формальні методи.
Більшість існуючих формальних методів (B-метод, Z, RAISE, VDM, TLA, та
інші) надають засоби підтримки доведення властивостей програмних систем. Такі
засоби в своїй основі мають програмні логіки.
Розробку програмних логік в своїх роботах розпочав T. Hoare, а
програмологія як напрямок інформатики бере свій початок в дослідженнях
В.Н. Редька. Дослідженнями програмних логік та формальних методів в цілому
активно займаються як вітчизняні вчені (С.В. Єршов, Г.М. Жолткевич,
С.Л. Кривий, О.А. Летичевський, А.М. Чеботарьов та інші) так і зарубіжні вчені
(L. Lamport, J. Reynolds, D. Harel, E. Clarke, D. Sannella, A. Tarlecki,
В.А. Непомнящий та інші).
Сучасні програмні логіки в тій чи іншій мірі базуються на логіці ФлойдаХоара. В таких логіках розглядаються предикати та функції скінченної арності,
причому предикати мають бути всюди визначеними. Існуючі розширення логіки
Флойда-Хоара також базуються на припущенні, що розглядаються лише всюди
визначені предикати. Проте при доведенні властивостей конкретних програмних
систем не завжди доводиться мати справу з тотальними предикатами, іноді
властивості можуть бути невизначеними на окремих даних. В такому випадку
потрібно використовувати спеціальні методи для того, щоб звести задачу до
випадку тотальних предикатів.
Програмні логіки з частковими предикатами повинні базуватись на
адекватних моделях програм. В дисертаційній роботі використовуються
композиційні-номінативні моделі програм, які розробляються на кафедрі теорії та
технології програмування факультету кібернетики Київського національного
університету імені Тараса Шевченка. У цих моделях стани програм подаються
6
номінативними (іменними) даними, семантика програм подається
відображеннями над номінативними даними, зокрема квазіарними
відображеннями, а засоби конструювання програм – композиціями відображень.
Композиційно-номінативні моделі програм дозволяють адекватним чином
формалізувати різні мови специфікацій та програмування, а також виступають
формальною основою відповідних програмних логік.
Вказані обставини обґрунтовують актуальність побудови програмних логік
квазіарних часткових предикатів та функцій над різними класами номінативних
даних, дослідження аксіоматичних систем побудованих логік та їх властивостей.
Зв'язок роботи з науковими програмами, планами, темами. Дисертаційна
робота є складовою частиною наукових робіт, які ведуться на кафедрі теорії та
технології програмування Київського національного університету імені Тараса
Шевченка при виконанні фундаментальних та прикладних тем: “Розробка
конструктивних математичних формалізмів для інтелектуальних систем
прийняття рішень, обробки знань, еталонування мов сучасних СУБД та CASEзасобів” (№ 0106U005856, 2006-2010 рр.), “Формальні специфікації та методи
розробки надійних програмних систем” (№ 0111U007052, 2011-2015 рр.),
“Розробка логіко-алгоритмічних методів дослідження формальних моделей
природних мов” (№ 0116U004780, 2016-2018 рр.).
Мета і завдання дисертаційного дослідження. Метою дисертаційної
роботи є розробка програмних логік композиційно-номінативного типу для
використання отриманих формальних систем в задачах специфікації та
верифікації програмних систем.
Із огляду на мету в роботі ставляться такі задачі:
 побудова програмної алгебри композиційно-номінативного типу для
простих номінативних даних;
 встановлення властивостей композицій програмного рівня побудованої
програмної алгебри;
 визначення композиційно-номінативної програмної логіки часткових
функцій та предикатів;
7
 розгляд існуючих аксіоматичних систем логіки Флойда-Хоара для
побудованої програмної логіки, дослідження коректності та повноти;
 побудова коректних та повних аксіоматичних систем з додатковими
обмеженнями;
 застосування отриманих результатів для дослідження програмних логік
та аксіоматичних систем для складних ієрархічних номінативних даних
та типізованих номінативних даних.
Об’єктом дисертаційного дослідження є програмні логіки часткових
предикатів та функції. Предметом дослідження є аксіоматичні системи для
програмних логік, питання їх повноти та коректності.
У роботі використовуються наступні методи: теоретико-множинні, теорії
програмування, математичної логіки, композиційно-номінативного підходу.
Наукова новизна одержаних результатів. Введено нові програмні алгебри
з узагальненими композиціями Флойда-Хоара та досліджено їх властивості.
Доведено монотонність та неперервність композицій запропонованих програмних
алгебр.
На основі розробленої програмної алгебри вперше побудовано програмні
логіки композиційно-номінативного типу для простих номінативних даних,
складних ієрархічних номінативних даних та типізованих номінативних даних.
Доведено що класичні аксіоматичні системи для побудованих програмних
логік часткових предикатів не є коректними. Вперше розроблено спеціальні
аксіоматичні системи з простими додатковими обмеженнями, аксіоматичні
системи з обмеженнями, що базуються на властивостях тверджень, які
виводяться. Доведено теореми про повноту та коректність побудованих
аксіоматичних систем для випадків простих та складних номінативних даних.
Теоретичне та практичне значення одержаних результатів. Дисертація
має теоретичну спрямованість. Теоретичне значення роботи полягає в
дослідженні програмного рівня композиційно-номінативних логік для різних
типів номінативних даних, визначенні основних властивостей композицій
програмного рівня.
8
Отримані результати були впроваджені у навчальний процес за
спеціальністю “Інформатика” на факультеті кібернетики Київського
національного університету імені Тараса Шевченка (нормативні курси “Теорія
програмування”, “Формальні методи розробки програмних систем”).
Практичне значення роботи полягає в застосуванні побудованих коректних
аксіоматичних систем для доведення властивостей програмних систем, та
дослідженні повноти відповідних аксіоматичних систем.
Особистий внесок здобувача. Всі результати дисертаційної роботи отримані
автором самостійно, сформульовані у вигляді теорем та строго доведені з
використанням допоміжних лем та тверджень, обґрунтовані з посиланнями на
використані джерела. Роботи [66, 67, 69, 71] написані здобувачем особисто і всі
результати, що містяться в них є оригінальними. Роботи [30, 31, 43, 44, 68, 70, 75,
77, 78] написані у співавторстві з науковим керівником Нікітченком М.С. У них
керівникові належать теоретичні ідеї і постановки задач, а дисертанту – практична
реалізація та доведення сформульованих теорем.
Апробація результатів дослідження. Основні положення та висновки
дисертаційного дослідження обговорювались на наукових семінарах кафедри
теорії та технології програмування Київського національного університету імені
Тараса Шевченка.
Результати дисертаційного дослідження оприлюднені у доповідях і
повідомленнях на Міжнародних та Всеукраїнських наукових конференціях,
семінарах: XVIII Міжнародній конференції “Knowledge–Dialogue–Solution” (KDS
2012, Київ, Україна, 2012 р.), XVI Міжнародній конференції “Dynamical System
Modelling and Stability Investigation” (DSMSI 2013, Київ, Україна, 2013 р.),
X Міжнародній конференції “Theoretical and Applied Aspects of Program Systems
Development” (TAAPSD’2013, Ялта, Україна, 2013 р.), II Міжнародній
конференції “Mathematics of Informational Modeling ” (MIM 2013, Варна, Болгарія,
2013 р.), IX Міжнародній конференції “Information and Communications
Technology in Education, Research and Industrial Applications” (ICTERI 2013,
Херсон, Україна, 2013 р.), 12-th International Conference on Informatics
9
(INFORMATICS’2013, Спішська Нова Вес, Словаччина, 2013 р.), XI Міжнародній
конференції “Theoretical and Applied Aspects of Program Systems Development”
(TAAPSD’2014, Київ, Україна, 2014 р.), Всеукраїнській науково-практичній
конференції “В.М. Глушков – Піонер Кібернетики” (Київський національний
технічний університет “КПІ”, Київ, Україна, 2014 р.)[30, 31, 43, 66, 67, 69, 70, 77].
Публікації. Основні результати дисертаційного дослідження опубліковано у
13 працях. Серед них – 5 статей у наукових журналах і збірниках наукових праць,
з них 3 статті опубліковано у фахових виданнях, затверджених ВАК України
[71,75,78], 2 статті опубліковано у наукових фахових іноземних журналах [44, 68];
8 тез та праць конференції.
Структура та обсяг дисертації. Дисертаційна робота складається зі вступу,
чотирьох розділів, висновків, списку використаних джерел (80 найменувань).
Загальний обсяг дисертації становить 130 с., основний зміст викладено на 118 с.

bibliography

ВИСНОВКИ
Основним результатом дисертації є дослідження програмних логік
композиційно-номінативного типу, що розв’язує завдання побудови коректних та
повних аксіоматичних систем відповідних програмних логік, і має суттєве
значення для розвитку формальних методів розробки програмного забезпечення
обчислювальних машин і систем. Зокрема:
1. Доведено монотонність та неперервність композицій для побудованих
композиційно-номінативних програмних алгебр часткових функцій та
предикатів над простими номінативними даними, наведено еквівалентні
перетворення для них.
2. Визначено синтаксичний та інтерпретаційний аспект програмних логік
композиційно-номінативного типу, що базуються на побудованих
програмних алгебрах.
3. Доведено, що і у випадках ієрархічних номінативних даних та типізованих
номінативних даних композиції програмних алгебр будуть монотонними
та неперервними. Побудовано програмні логіки складних номінативних
даних, семантика яких задається за допомогою відповідних програмних
алгебр
4. Для програмних логік доведено, що класична аксіоматична система,
запропонована для мови WHILE, не є коректною.
5. Розроблено аксіоматичну систему з доданими обмеженнями, що є
коректною та екстенсіонально повною. Показано, що аналогічна
аксіоматична система може бути побудована як для програмних логік над
ієрархічними номінативними даними, так і для програмних логік над
типізованими номінативними даними.
6. Побудовано аксіоматичну систему зі спрощеними обмеженнями в якій
виводяться лише твердження для яких виконується умова T-зростання,
також побудовано дуальну F-спадну аксіоматичну систему. Доведено їх
коректність та показано, що вони не будуть екстенсіонально повними для
122
всіх тверджень, проте T-зростаюча аксіоматична система буде
екстенсіонально повною для достатньо широкого класу тверджень.
7. Поєднуючи підходи, використані для побудови коректних аксіоматичних
систем за допомогою додаткових обмежень, отримано коректну та
екстенсіонально повну систему з додатковими обмеженнями.
8. Доведено теореми про повноту та коректність аксіоматичних систем для
випадків складних номінативних даних.
Слід відмітити, що при переході від логіки Флойда-Хоара, в якій
розглядались лише тотальні предикати скінченної арності, до програмних логік
часткових квазіарних предикатів над номінативними даними, аксіоматична
система не є коректною. Це зумовило проблему пошуку шляхів модифікації
аксіоматичної системи, щоб вона була коректною. Одним з таких шляхів є
визначення додаткових умов для правил. В роботі продемонстровано, що існує
також багато підходів до введення додаткових умов. Таким чином було отримано
різні коректні аксіоматичні системи. Проте деякі з них були надлишковими, а
деякі не були повними.
Варто зазначити, що для кожної аксіоматичної системи програмної логіки
композиційно-номінативного типу над простими номінативними даними, аналоги,
побудовані для програмних логік над складнішими номінативними даними,
зберігали властивості бути коректними та екстенсіонально повними.