Омельчук Людмила Леонідівна. Аксіоматичні системи cпецифікацій програм над номінативними даними : Дис... канд. наук: 01.05.01 - 2007.
Анотація до роботи:
Омельчук Л.Л. Аксіоматичні системи cпецифікацій програм над номінативними даними. – Рукопис.
Дисертація на здобуття наукового ступеня кандидата фізико-математичних наук за спеціальністю 01.05.01 – теоретичні основи інформатики та кібернетики. – Київський національний університет імені Тараса Шевченка. – Київ 2007.
На основі композиційно-номінативного підходу побудовані та досліджені імперативні та декларативні моделі недетермінованих програм. Семантика таких програм задається частковими багатозначними функціями (бінарними відношеннями) над номінативними даними. Визначено повний клас натурально обчислюваних функцій такого типу та наведено його алгебраїчне подання. В роботі визначено спеціальний вид обчислюваності – номінативна обчислюваність. Номінативна обчислюваність дозволяє адекватно визначити повний клас обчислюваних функцій над номінативними даними. Номінативна обчислюваність орієнтована на функції і композиції, близькі до програмних функцій і композицій. Будується аксіоматична теорія номінативних даних, яка спроможна специфікувати усі номінативно обчислювані функції.
Побудовано прототип реалізації аксіоматичної системи специфікацій програм над номінативними даними, а також продемонстровано, що він дозволяє доводити деякі властивості програм.
Головний результат дисертаційної роботи – розробка та дослідження композиційно-номінативних аксіоматичних систем для специфікацій програм, що орієнтовані на роботу зі структурованими даними, розв’язують практично важливі задачі специфікації програм та мають істотне значення для теорії і практики програмування.
В роботі запропоновано новий підхід до побудови аксіоматичних систем специфікацій програм над номінативними даними, в основі якого лежить композиційно-номінативний метод уточнення поняття програми. В результаті проведеної роботи:
побудовано клас моделей програм, що базуються на номінативних та, зокрема, метаномінативних типах даних;
визначено спеціальний вид обчислюваності – номінативну обчислюваність, яка базується на системі базових функцій і композицій, близьких до функцій та композицій мов програмування, та доведено співпадіння повного класу номінативно обчислюваних функцій з повним класом натурально обчислюваних функцій над номінативними даними;
доведено, що кожна частково рекурсивна функція може бути представлена номінативно обчислюваними функціями;
визначено та досліджено аксіоматичну теорію номінативних даних, яка дозволяє доводити низку важливих властивостей часткових багатозначних функцій (бінарних відношень);
побудовано прототип реалізації аксіоматичної системи специфікацій програм над номінативними даними, який базується на секвенційному численні композиційно-номінативних логік, використовує синтаксичну нотацію близьку до мови специфікацій програм Z та забезпечує доведення властивостей програм.
Публікації автора:
Омельчук Л.Л. Обчислюваність функцій над метаномінативними даними // Вісн. Київ. ун-ту. Сер.: фіз.-мат. науки. – 2001. – Вип.1. – С . 275-286.
Омельчук Л.Л. Секвенційне числення для композиційно-номінативних логік часткових предикатів // Вісн. Київ. ун-ту. Сер.: фіз.-мат. науки. – 2003. – Вип.4. – С. 270–278.
Омельчук Л.Л Система автоматизації доведення теорем теорії метаномінативних даних // Вісн. Київ. ун-ту. Сер.: фіз.-мат. науки. – 2006. – Вип.2. – С. 231–235.
Нікітченко М.С., Шкільняк С.С., Омельчук Л.Л. Логіки, орієнтовані на специфікації програм // Проблеми програмування. – 2006. – № 2-3. – С.17-24.
Омельчук Л.Л. Секвенциальные исчисления логик частичных предикатов // Dynamical system modelling and stability investigation. – Thesis of conference reports. – Kyiv, Ukraine, 2003. P. 410.
Омельчук Л.Л. Аксіоматичні системи для мов специфікацій програм Theoretical and applied aspects of program systems development (TAAPSD’2004). – Abstracts. – Kyiv, Ukraine, 2004. P. 57-61.
Nikolaj Nikitchenko, Ludmila Omelchuk, Stepan Shkilniak: Formalisms for Specification of Programs over Nominative Data // Electronic computers and informatics (ECI 2006). – Thesis of conference reports. – Koice – Herany, Slovakia, 2006. P. 134-139.
Омельчук Л.Л. Система специфікацій програм над номінативними даними // Theoretical and applied aspects of program systems development (TAAPSD’2006). – Abstracts. – Kyiv, Ukraine, 2006. P. 96-100.
