Шевченко Руслан Сергійович Розробка системи TermWare для аналізу та побудови програм на основі переписувальних правил

Краткое описание

Шевченко Руслан Сергійович, директор ТОВ «ГрадСофт». Назва дисертації: «Розробка системи TermWare для аналізу та побудови програм на основі переписувальних правил». Шифр та назва спеціальності 01.05.03 математичне та програмне забезпечення обчислювальнихмашинісистем. Спецрада Д26.001.09 Київського національного університету імені Тараса Шевченка

Національна академія наук України
Інститут програмних систем
Міністерство освіти та науки України
Київський національний університет імені Тараса Шевченко
Кваліфікаційна наукова праця
на правах рукопису
Шевченко Руслан Сергійович
УДК 004.424
ДИСЕРТАЦІЯ
РОЗРОБКА СИСТЕМИ TERMWARE ДЛЯ АНАЛІЗУ ТА ПОБУДОВІ
ПРОГРАМ НА ОСНОВІ ПЕРЕПИСУВАЛЬНИХ ПРАВИЛ
01.05.03 – математичне та програмне забезпечення
обчислювальних машин і систем
Подається на здобуття наукового ступеня
кандидата технічних наук
(12 – інформаційні технології)
Дисертація містить результати власних досліджень. Використання ідей,
результатів і текстів інших авторів мають посилання на відповідне джерело.
________ Р.C. Шевченко.
Науковий керівник: Дорошенко Анатолій Юхимович
професор, доктор фізико-математичних наук
Київ – 2021

Зміст
Перелік Позначень ................................................................................................ 11
Вступ....................................................................................................................... 13
Розділ 1. Огляд існуючих підходів до систем переписування та мотивація
підходу TermWarw . .............................................................................................. 19
1.1. Огляд напрямку. ........................................................................................................................... 19
1.1.1. Типологія систем переписувальних правил. ................................................................. 19
1.1.2. Теоретичні моделі переписувальних правил................................................................ 20
1.1.3. Застосування переписування для задач програмної інженерії. .......................... 26
1.2. Система TermWare/Java............................................................................................................ 28
1.2.1. Призначення та мотивація створення.............................................................................. 28
1.2.2. Формальна модель TermWare. .............................................................................................. 31
1.2.3. Реалізація теоретичної моделі у мові програмування. ............................................ 36
1.2.4. Вбудовування TermWare у програмні комплекси. ..................................................... 38
1.3. Висновки до Розділу 1. .............................................................................................................. 43
1.4. Список використаної літератури до Розділу 1. ............................................................ 43
Розділ 2. Математичні моделі перетворювання термів..................................... 50
2.1. η-числення................................................................................................................................................. 50
2.1.1. Формальні моделі η-числення...................................................................................................... 51
2.1.1.1. Безтипове η-числення................................................................................................................... 51
2.1.1.2. Операційна семантика. ................................................................................................................. 53
2.1.1.3. Інтенсіональна рівність як заміна перейменування змінних .................................. 55
2.1.2. Комбінування правил у впорядковані множини................................................................ 57
2.1.3. Доповнення η-числення операціями взаємодії з середовищем за
допомогою θ-конструкції............................................................................................................................ 60
2.1.4. Типизоване η-числення ................................................................................................................... 61
2.2. Числення контекстних термів ......................................................................................................... 64
2.2.1. Основні конструкції числення контекстних термів. ........................................................ 65
2.2.2. Уніфікація контекстних термів.................................................................................................... 66
2.2.3. Множинні мультітерми та операції роботи з контекстом............................................. 68
2.2.4. Моделювання систем типів за допомогою контекстних термів. ............................... 74
10
2.2.5. Розширення контекстного числення диз’юктивними та
кон’юктивними мультітермами.............................................................................................................. 78
2.3. Висновки до Розділу 2. ......................................................................................................................... 81
2.4. Список використаної літератури до Розділу 2. ....................................................................... 82
Розділ 3. Застосування TermWare........................................................................ 85
3.1. Побудова високорівневого опису бізнес-логіки:.................................................................... 85
3.2. Моделювання сенсорних мереж: .................................................................................................... 90
3.3. Застосування TermWare для аналізу програмного коду.......................................102
3.3.1. Використовування систем правил для переписування AST.......................................102
3.3.2. Типологія програмних помилок................................................................................................105
3.4. Семантичні модельні терми...........................................................................................................114
3.5. Реалізація TermWare3. Основні відмінності версій ............................................................122
3.6. Застосування до аналізу смарт контрактів:............................................................................125
3.7. Висновки до Розділу 3. .......................................................................................................................130
3.8. Список використаної літератури до Розділу 3. .....................................................................131
Висновки .............................................................................................................. 134
Загальний список використаних джерел. ......................................................... 136
Додатки................................................................................................................. 147
Додаток 1: Правила JavaChecker для знаходження витоку ресурсів:.................................147
Додаток 2: Правила для часткової інтерпретації java коду:...................................................149
11
Перелік Позначень
API – Application Programming Interface. Програмний Інтерфейс Взаємодії
AST – Abstract Syntax Tree. Абстрактне синтаксичне дерево
BPML – Business Process Modelling Language. Мова моделювання бізнес
процессів.
CCM – Change and Configuration Management. Управління змінами та
конфігураціями.
CHAM – Chemical Abstract Machine. Хімічна абстрактна машина
CPU – Central Processing Unit. Центральний Процесор.
CRS – Combinatory Reduction Systems. Комбінаторні редуктивні системи
CRM – Customer Relationship Management. Система обліку кліентів.
CTRS – Conditional Term Reduction System. Системи Умовної Редукції
Термів.
DB – Database. База даних.
DSL – Domain Specific Language. Проблемно Орієнтовна Мова
IDE – Integrated Development Environment. Інтегроване середовище розробки.
IDEF – Integrated DEFinition Method. Інтегрована методологія моделювання
систем.
IDL – Interface Definition Language. Мова визначення інтерфейсів
JVM – Java Virtual Machine. Віртуальна Java Машина.
GPU – Graphics Processor Unit. Графічний прискорювач.
HOAS – Hight Order Abstract Syntax. Абстрактний Синтакс Вищого Порядку
OS – Operation Sysgem. Операційна система
RAD – Rapid Application Development. Швидка Розробка Застосувань.
TRS – Term Reduction System, Cистеми Редукціх Термів
UML – Unified Modelling Language. Уніфікована мова моделювання.
VM – Virtual Machine. Віртуальна Машина
WSDL – Web Service Definition Language. Мова визначень веб-сервісів.
12
XML – eXtensible Markap Language. Розширбвана мова розмітки.
ПЗ – Програмне Забезпечення
БД – База даних
13
Вступ
Актуальність
У наш час сфера створення нових формальних систем та аналізу
існуючих бурхливо розвивається, що пов'язано з зростанням складності
програмних систем та необхідністю створення нових засобів їх опису.
З кожним роком все більше аспектів людського життя, прямо чи
опосередковано, стає тісно пов’язаним з контролюючим програмним
забезпеченням. Кількість коду зростає експоненціальним чином, проте
людські можливості його написання та аналізу обумовлені біологічно та
залишаються приблизно на тому рівні, що був під час створення перших
програмних систем.
Системи переписувальних правил є одним з фундаментальних підходів
до аналізу та опису програмних систем. Можливість їхньої програмної
реалізації відкриває шлях до скорочення відстані між абстрактним численням
та прагматикою перетворення коду.
Подальший прогрес у продуктивності обчислень також пов’язаний з
розробкою нових архітектур обчислювальних систем з підтримкою масового
паралелізму та спеціалізованих процесорів. Розвиток апаратного
забезпечення обчислювальної техніки має супроводжуватись створенням
програмних засобів, що дозволяють використовувати нові можливості.
Одним з перспективних напрямків є автоматичне перетворення програм, що
дозволяє, зберігаючи незмінним первісний програмний код, отримати його
спеціалізацію для широкого спектру обраних архітектур.
Можна сказати, що будь-який оптимізуючий компілятор містить у собі
спеціалізовану сиcтему переписувальних правил. Системи переписувальних
правил загального призначення можуть стати основою для наступного
покоління компіляторів, де вхідна мова буде визначатись конфігурацією
14
переписувальних правил. Система інтеграції переписувальних правил з
семантичними аналізаторами мов програмування може полегшити побудову
аналізаторів програмного коду.
У відділі теорії комп’ютерних обчислень Інституту програмних систем
НАНУ упродовж тривалого періоду розвивається напрямок досліджень,
пов’язаний з розробкою теорії та інструментальних засобів для
автоматизованого проєктування паралельних і розподілених програм. Цей
напрямок, що бере початок у працях В. М. Глушкова, Г. О. Цейтліна та К. Л.
Ющенко з розробки систем алгоритмічних алгебр та їх модифікацій,
продовжений в роботах С.Д. Погорілого, Л.Д. Акуловського та інших
дослідників. Перетворення алгоритмів на основі техніки переписувальних
правил розвивається відомою системою алгебраїчного програмування APS
від О.А. Летичевського та його школи, а також системою TermWare,
розробленою в Інституті програмних систем НАНУ.
У фокусі даної роботи є реалізація та застосування системи
переписувальних правил TermWare та побудова відповідного числення.
TermWare – це реалізація системи переписувальних правил, призначена для
роботи з програмним кодом: аналізу, трансформації та генерації програм.
Зв'язок роботи з науковими програмами, планами, темами.
Дисертаційна робота виконувалась у рамках наступних науково-дослідних
робіт:
1. "Застосування методів автоматизації проектування для розробки
високопродуктивних програм обробки наукових даних на cloud-платформах",
№ держреєстрації 0116U003303.
2. "Розробка алгеброалгоритмічних методів, технологій та засобів
автоматизації паралельного програмування для неоднорідних та cloudплатформ", № держреєстрації 0117U000734.
3. "Розробка прикладних програмних засобів високопродуктивних обчислень
для ефективного розв’язання задачі прогнозування метеорологічних процесів
15
на території України на основі відеографічних прискорювачів", №
держреєстрації 0114U005005.
4. "Розробка формальних та адаптивних методів, технологій та засобів
паралельного програмування для неоднорідних мультипроцесорних
обчислювальних систем", № держреєстрації 0112U002760.
Мета і завдання дослідження.
Метою дослідження є побудова інструментальних засобів роботи з
переписувальними правилами для використання у програмній інженерії:
системах обробки та перетворення програмного коду та інтерпретації
прикладних проблемно орієнтованих мов.
Для досягнення цієї мети були поставлені наступні завдання:
1. Розробити систему переписувальних правил загального призначення,
що може бути вбудована у прикладні системи користувача.
2. Дослідити теоретичні моделі переписувальних правил для побудови
високорівневої проблемно-орієнтованої мови представлення правил.
3. Розробити модульну системи підключення адаптерів синтаксису та
семантики мов програмування, для подання програмного коду у
вигляді термів для аналізу та перетворення, та відповідно, термів у
синтаксисі вибраної мови для їх генерування.
4. Розробити адаптери для мов Java та CORBA IDL, систему аналізу коду
для сканування та виявлення дефектів кодування, що заснована на
TermWare, декількох прикладних систем для автоматизації
генерування моделей баз даних.
5. Впровадити інструментальні засоби на основі отриманої системи у
процесс розробки прикладного програмного забезпечення.
Предметом дослідження є процеси автоматизації аналізу та перетворення
виразів у формальних мовах у вигляді переписувальних правил.
Об'єктом дослідження є засоби моделювання, аналізу та генерації систем
формальних мов, включаючи мови програмування та опису бізнес-процесів.
16
Методи дослідження. У роботі використано методи дискретної математики,
математичної логіки та теорії переписувальних систем, формалізацію,
конструювання формального числення, моделювання операційної семантики
перетворень.
Наукова новизна.
1. Вперше побудовано числення контекстів, що додає до існуючих
технік переписувальних правил засоби роботи з контекстом, що
міститься в термах, що значно спрощує роботи з іерархічними
контекстами в мовах програмування.
2. Запропоновано нову модель інтеграції сукупності переписувальних
правил та інтерфейсу з зовнішнім середовищем у формі бази фактів,
що дозволяє описувати базу фактів у вигляді імперативного коду,
підключати адаптери мов програмування та модулі семантики, а
також підключати системи переписування в інші системи в якості
бібліотек.
3. Побудовано нову лінійку версій реалізації систем переписувальних
правил TermWare, що заснована на цій моделі інтеграції, де кожна
наступна версія є удосконаленням попередньої.
4. Розроблену нову систему переписування TermWare і
продемонстроване практичне застосовання в кількох прикладних
галузях: моделювання сенсорних систем, аналіз та генерація
програмного коду, оптимізація і розпаралелювання програм.
Практичне значення результатів.
Серія систем переписувальних правил TermWare використовується для
широкого спектру прикладних задач, таких як:
- Аналіз програмного коду: статичний аналізатор програм на мові Java
(JavaCheker) побудовано у середовищі алгебраїчного програмування
TermWarе.
17
- Формалізація побудови паралельних алгоритмів: використовування
високорівневого інструментарію алгоро-алгебраїчного проєктування,
доповненого підсистемою переписувальних правил та низькорівневих
профіліруючих засобів, для автоматизації проєктування та підвищення
продуктивності послідовних та паралельних (багатопоточних) програм з
загальною пам’яттю.
- Спеціалізація програмного коду за допомогою часткового виконання.
- Автоматичне генерування схем баз данних на основі структури
об’єкту.
Систему впроваджено у ТОВ. IMATEK як частину програмноаппаратного комплексу документообігу підприємств та програмного
комплексу для аналізу виробничих процессів, що впроваджено у 28
підпріємствах та державних установах; у ТОВ. Кіглі як інструментальний
засіб для що організує перевірку функціональних програм та алгоритмів.
Акт впровадження наведені у додатку
Особистий внесок здобувача.
- Представлені до захисту результати були отримані здобувачем
особисто. В опублікованих у співавторстві роботах [2],[3],[5],[6],[11]
дисертанту належить реалізація системи переписувальних правил TermWare,
теоретичні моделі переписувальних систем та виконання експерименальних
робіт. Науковому керівнику Дорошенко А.Ю. належить постановка задачі та
участь в систематизації одержаних результатів. В роботі [9] Яценко О.А.
належить частина розробленого розпаралелюючого засобу поверх TermWare,
що відповідає за виконання трансформації програми за допомогою
інструментарію проектування та синтезу програм. В роботі [1] Жеребу К. А.
належить частина, що відповідає за представлення мережевих протоколів у
вигляді TermWare термів та інтеграція і експериментальні роботи з системою
імітаційного моделювання.
18
Апробація результатів дисертації.
Результати роботи апробовані на наступних конференціях:
• CONCURRENCY SPECIFICATION AND PROGRAMMING (CS&P
2005) Ruciane-Nide, Poland, 28–30 September 2005.
• Шоста міжнародна науково-практична конференція з програмування
УкрПРОГ'2008, 27-29 травня 2008 р., Україна, Київ.
• Scala Symposium 2016. Amsterdam, October 2016.
• Одинадцята міжнародна науково-практична конференція з
програмування УкрПРОГ’2018. Україна, Київ.
• Міжнародна Науково-Практична Конференція Winter INFOCOM’2018
Advanced Solutions VII. Україна, Київ.
Публікації. Основний зміст роботи викладено в 11 друкованих
працях, серед яких 9 статей у фахових виданнях ВАК України, 2 статті у
фахових закордонних журналах та у 3 тезах конференцій.
Структура та обсяг роботи. Дисертація складається зі вступу, трьох
розділів, висновків, 2 додатків та переліку використаної літератури з 99
посилань.

Список литературы

Висновки
У дисертаційній роботі розроблені методи реалізації систем
переписувальних правил, розроблена лінійка TermWare, описана та
формалізована теоретична модель для систем переписувальних правил з
інтеракцією. Отримані наступні результати, що мають наукову і практичну
цінність:
• Розроблено η-числення, що вдосконалює теоретичні моделі для
класу систем переписування з впорядкованими правилами; числення
контекстів, що вперше додає до існуючого математичного апарату
переписувальних правил засоби роботи з контекстом.
• Побудована нова реалізація систем переписувальних правил
загального призначення TermWare з підтримкою інтеграції
сукупності переписувальних правил та інтерфейсу з зовнішнім
середовищем, що дозволяє:
o вбудувати систему роботи з переписувальними правилами у
систему користувача як бібліотеку;
o інтегрувати імперативне представлення бази фактів
користувача з семантикою переписувальних правил;
o підключити адаптери представлення формальних мов,
включаючи мови програмування, у вигляді термів.
• Розроблена нова модульна система підключення адаптерів
синтаксису та семантики мов програмування, для подання
програмного коду у вигляді термів для аналізу та перетворення, та,
відповідно, термів у синтаксисі вибраної мови для їх генерування.
• Розроблені адаптери для мови Java та CORBA IDL, системи аналізу
коду JavaChecker для сканування та виявлення дефектів кодування,
135
що заснована на TermWare, декількох прикладних систем для
автоматизації генерування моделей баз данних.
• Впроваджено рішення на основі TermWare застосовуються у
програмно-апаратному комплексі документообігу ІМАТЕК-ЕСКО,
що впроваджені на більш ніж 28 підприємствах та державних
установах; впроваджено рішення для сканування та перевірки коду
системи моніторингу рухомих об’єктів у ТОВ Кіглі.