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

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

Омельчук Людмила Леонідівна

УДК 681.3

АКСІОМАТИЧНІ СИСТЕМИ СПЕЦИФІКАЦІЙ ПРОГРАМ

НАД НОМІНАТИВНИМИ ДАНИМИ

01.05.01 – теоретичні основи інформатики та кібернетики

Автореферат

дисертації на здобуття наукового ступеня

кандидата фізико-математичних наук

Київ – 2007

Дисертацією є рукопис.

Робота виконана на кафедрі теорії та технології програмування факультету

кібернетики Київського національного університету імені Тараса Шевченка.

Науковий керівник: доктор фізико-математичних наук, професор

Нікітченко Микола Степанович,

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

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

завідувач кафедри теорії та технології програмування

Офіційні опоненти: доктор фізико-математичних наук, професор

Лавріщева Катерина Михайлівна,

Інститут програмних систем НАН України, м. Київ,

завідувач відділу програмної інженерії

кандидат фізико-математичних наук, доцент

Глибовець Микола Миколайович,

Національний університет “Києво-Могилянська академія”, МОН України, м. Київ,

декан факультету інформатики

Провідна організація: Інститут кібернетики НАН України, м. Київ,

відділ оптимізації керованих процесів

Захист відбудеться “5” квітня 2007 р. о 14 годині на засіданні спеціалізованої вченої ради Д 26.001.09 Київського національного університету імені Тараса Шевченка за адресою: 03127, Київ, пр. Глушкова, 2, корп. 6, ф-т кібернетики, ауд. 40. (Тел. 521-33-66. Факс 259-70-44. E-mail: rada1@unicyb.kiev.ua)

З дисертацією можна ознайомитись у Науковій бібліотеці Київського національного університету імені Тараса Шевченка за адресою:

01033, Київ, вул. Володимирська, 58.

Автореферат розісланий “3” березня 2007 р.

Вчений секретар спеціалізованої вченої ради Д.Я. Хусаїнов

ЗАГАЛЬНА ХАРАКТЕРИСТИКА РОБОТИ

Актуальність теми. Постійне розширення сфери застосування інформаційних технологій загострює проблему швидкого та економічного конструювання надійного програмного забезпечення. На сьогоднішній день запропоновано різні методи систематичного та практичного програмування, які мають на меті покращення якості створюваних програмних систем. Серед методів систематичного програмування виділяють: структурний, модульний, компонентний, аспектно-орієнтований, об’єктно-орієнтованане проектування та моделювання. Одночасно з практичними методами розробки програмних систем розвивалися і теоретичні методи, зокрема, алгебраїчне, інсерційне, агентне, композиційне, експлікативне програмування. Ці методи базуються на алгебраїчних, алгоритмічних та логіко-математичних підходах до формальної побудови та доведення програм.

Авторами української теоретичної школи програмування (П.І. Андон, А.В. Анісімов, Д.Б. Буй, А.Ю. Дорошенко, Ю.В. Капітонова, С.Л. Кривий, К.М. Лавріщева, О.А. Летічевський, М.С. Нікітченко, В.Н. Редько, Г.О. Цейтлін, С.С. Шкільняк та іншими) створені нові методи розв’язання проблем програмування. Особливого розвитку зазнала теорія алгебраїчного програмування, яка забезпечує опис математичних конструкцій, обчислень, алгебраїчних перетворень, доведення математичних теорем.

Одним з підходів до специфікації програмного забезпечення є композиційне (експлікативне) програмування (КП), яке започатковане академіком НАН України, доктором фізико-математичних наук, проф. В.Н. Редьком та розвивається на кафедрі теорії та технології програмування факультету кібернетики Київського національного університету імені Тараса Шевченка. КП є розвитком структурологічного підходу Г. Фреге, який був перенесений на програмування А.А. Ляпуновим та розвинений Ю.І. Яновим, А.П. Єршовим, Л.О. Калужніним, В. М. Глушковим та іншими. В КП досліджуються системи на різних рівнях абстракції, які виникають на шляху експлікації програмування – абстрактному, булевському та номінативному (атрибутному) рівнях. Системи останнього рівня, які базуються на композиційно-номінативних методах, запропонованих М.С. Нікітченком, є досить багатими для адекватного задання моделей структур даних, програм та засобів їх конструювання.

Останнім часом, серед практичних методів проектування програмного забезпечення (ПЗ) значного розповсюдження набуло об’єктно-орієнтоване проектування (ООП) програмних систем. Визначилась технологічна база розробки різних видів програмного забезпечення методами ООП (зокрема UML – Unified Modeling Language).

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

Як правило, мови специфікацій програм базуються на традиційному теоретико-множинному підході до формалізації програм та, зазвичай, використовують аксіоматику множин Цермело-Френкеля (ZF). Застосування такого розвинутого формалізму до проблем розробки програм дозволяє досить ефективно розв’язувати певні прикладні проблеми. Ця теорія є достатньо потужною, разом з цим, її адекватність програмуванню (адекватність семантики, структур даних, композицій) залишається недостатньою. Зазначені питання роблять актуальною проблему пошуку нових підходів, які можуть привести до побудови більш адекватних формалізмів специфікацій програм. Таким чином, створення аксіоматичної системи специфікацій програм над номінативними даними є актуальною проблемою.

Зв’язок роботи з науковими програмами, планами, темами.

Дисертаційна робота виконувалася в рамках комплексної наукової програми Київського національного університету імені Тараса Шевченка “Інформатизація суспільства” (теми “Логіко-математичні та програмологічні засоби інформаційних технологій”, (2001-2005, номер держреєстрації – 0101U002163), “Еталонування семантичних структур мов CASE-середовищ програмологічними засобами”, (2001-2005, номер держреєстрації – 0101U005770), замовник – Фонд фундаментальних досліджень Міністерства освіти і науки України, а також теми “Розробка конструктивних математичних формалізмів для інтелектуальних систем прийняття рішень, обробки знань, еталонування мов сучасних СУБД та CASE-засобів”, (2006-2010, номер держреєстрації – 0106U005856), замовник – Міністерство економіки України).

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

Досягнення мети пов’язано з розв’язком наступних задач:

проведення порівняльного аналізу методів формальних специфікацій;

побудова номінативної та, зокрема, метаномінативної моделей даних;

дослідження обчислюваності функцій над класом номінативних даних;

побудова аксіоматичних систем для композиційно-номінативних мов специфікацій програм над номінативними даними;

побудова прототипу реалізації аксіоматичної системи специфікацій програм над номінативними даними.

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

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

В дисертаційній роботі застосовано композиційно-номінативний метод уточнення поняття програми до побудови аксіоматичних систем специфікацій програм. Теорія номінативних множин, що запропонована в роботі, розвивається в дусі теорії допустимих множин (С. Кріпке, Р. Платек, Дж. Барвайз, Ю.Л. Єршов). Завдяки застосуванню композиційно-номінативного підходу з’являється можливість побудови аксіоматичних систем специфікацій програм на єдиній концептуальній основі, а також, це дозволяє достатньо адекватно задавати складні типи даних. В роботі розроблено прототип реалізації аксіоматичної системи специфікацій програм над номінативними даними. Ця система побудована на основі композиційно-номінативного методу уточнення поняття програми та використовує синтаксичну нотацію, близьку до нотації відомої мови специфікацій програм Z.

Наукова новизна одержаних результатів полягає в наступному:

побудовано клас моделей програм, заснованих на номінативних та, зокрема, метаномінативних типах даних;

визначено новий вид обчислюваності – номінативну обчислюваність, яка базується на системі базових функцій і композицій, близьких до функцій та композицій мов програмування;

доведено, що будь-яка частково рекурсивна функція (ЧРФ) може бути представлена номінативно обчислюваними функціями;

доведено, що повний клас номінативно обчислюваних функцій збігається з повним класом натурально обчислюваних функцій над номінативними даними;

визначено та досліджено нову аксіоматичну теорію номінативних даних, яка є достатньо багатою та дозволяє доводити низку важливих властивостей часткових багатозначних функцій (бінарних відношень).

Практичне значення одержаних результатів

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

Результати роботи використовуються в навчальному процесі при підготовці та читанні курсів “Математична логіка”, “Теорія алгоритмів”, “Програмування” та “Формальні методи специфікацій програм” на факультеті кібернетики Київського національного університету імені Тараса Шевченка.

Особистий внесок здобувача. Всі основні результати дисертації одержані автором самостійно. У спільно виконаних з науковим керівником д.ф.-м.н. Нікітченком М.С. та к.ф.-м.н. Шкільняком С.С. роботах пошукувачем досліджено аксіоматичні системи специфікацій програм, в основі яких лежить композиційно-номінативний метод уточнення поняття програми, побудовано прототип реалізації такої системи, та продемонстровано, що він дозволяє доводити деякі властивості програм. Зокрема:

в роботі [4] – пошукувачу належить розділ: “Автоматизована система доведення теорем теорії метаномінативних даних”;

в роботі [7] – пошукувачу належить розділ: “A prototype of a theorem proving system”.

Апробація результатів дисертації. Результати проведених досліджень обговорювались на конференціях та самінарах факультету кібернетики Київського національного університету імені Тараса Шевченка, Інституту кібернетики НАН України. Основні наукові результати доповідались на наступних наукових конференціях:

Dynamical system modelling and stability investigation, Kyiv, Ukraine, 2003.

Theoretical and applied aspects of program systems development (TAAPSD’2004), Kyiv, Ukraine, 2004.

П’ята міжнародна науково-практична конференція з програмування (УкрПРОГ'2006) Київ, Україна, Кібернетичний центр Національної академії наук України, 2006.

Electronic computers and informatics (ECI 2006), Koљice – Herѕany, Slovakia, 2006.

Theoretical and applied aspects of program systems development (TAAPSD’2006), Kyiv, Ukraine, 2006.

Публікації. За темою дисертації опубліковано 8 наукових праць, 4 – статті у фахових виданнях наукових праць, які затверджені ВАК України, 4 – публікації у збірках матеріалів науково-практичних конференцій.

Структура та обсяг роботи. Дисертаційна робота складається із вступу, п’яти розділів, висновків, списку використаних джерел (114 найменувань), додатків А та Б. Загальний обсяг роботи становить 142 сторінки, основний текст роботи викладено на 124 сторінках.

Основний зміст роботи

У вступі обґрунтовано актуальність роботи, наведено короткий огляд основних результатів та відкритих проблем досліджуваної галузі, сформульована мета дисертації, описані отримані результати, відмічається їх новизна та практичне значення. Вступ також містить огляд структури дисертації.

У першому розділі “Огляд основних методів та мов специфікацій програм” досліджено різні стилі і методи математичних специфікацій. Зокрема, в дисертації детально розглянуто специфікації поведінки систем. Описані основні типи таких специфікацій: специфікації абстрактної моделі, алгебраїчні, специфікації переходів станів, аксіоматичні, часові логічні специфікації.

Деякі особливості різних стилів і методів формальних специфікацій програм проілюстровано на прикладі адресної книги.

У підрозділі 1.1 досліджено деякі особливості специфікацій абстрактної моделі та аксіоматичних специфікацій на прикладі мов Z та VDM. Зокрема, у пункті 1.1.1 розглянуто Z специфікації, а в пункті 1.1.2 досліджено специфікації на мові VDM для запропонованого прикладу, а також зроблено порівняння мов Z та VDM. У підрозділі 1.2 проаналізовано метод Clear як приклад алгебраїчної мови специфікацій. У підрозділі 1.3 розглядається метод RAISE як приклад специфікації абстрактної моделі.

Перераховані мови специфікацій програм базуються на традиційному теоретико-множинному підході до формалізації програм та використовують аксіоматику множин Цермело-Френкеля (ZF). Застосування такого розвинутого формалізму до проблем розробки програм дозволяє досить ефективно розв’язувати певні прикладні проблеми. Ця теорія є достатньо потужною, разом з цим, її адекватність програмуванню (адекватність семантики, структур даних, композицій) залишається недостатньою. Зазначені питання роблять актуальною проблему пошуку нових підходів, які можуть привести до побудови більш адекватних формалізмів специфікацій програм.

В дисертаційній роботі застосовано композиційно-номінативний метод уточнення поняття програми до побудови аксіоматичних систем специфікацій програм.

У другому розділі “Основні методологічні положення композиційно-номінативного методу” запропоновано підхід до формальної специфікації програм, основою якого є:–

сформульовані основні принципи композиційно-номінативного методу;–

визначені основні поняття та позначення для часткових багатозначних функцій;

запропоновані композиційно-номінативні системи;

досліджені номінативні дані, функції та композиції над ними;

досліджені метаномінативні дані, функції та композиції над ними;

визначені імперативні та предикатні композиційно-номінативні системи.

Застосований підхід надає єдину методологічну основу для формалізації специфікацій програм, доведення їх властивостей, а також для проведення їх подальшої конкретизації до мов програмування більш низького рівня. Підхід спирається на базові принципи композиційно-номінативного методу, а саме принципи: розвитку (від абстрактного до конкретного), апплікативності (функціональності), номінативності програм, композиційності, дескриптивності, номінативності даних, обчислюваності, теоретико-функціональної формалізації.

Функція трактується як часткова багатозначна функція (бінарне відношення). Цей клас функцій застосовується для представлення семантики недетермінованих програм. Основні використовувані поняття і позначення для часткових багатозначних функцій, а також деякі властивості цих функцій наведено у підрозділі 2.2.

На верхніх рівнях абстракції поняття програми уточнюється за допомогою композиційно-номінативних систем (КНС), які запропоновано у підрозділі 2.3. Визначено різні рівні композиційних систем: абстрактний, булевський, номінативний та метаномінативний. Підкреслюється, що основну роль у програмуванні відіграють дані номінативного та метаномінативного рівнів, оскільки структури даних абстрактного і булевського рівня бідні.

У підрозділі 2.4 дано опис номінативних даних, функцій та композицій над ними. Клас ND інфінітарних номінативних даних будується у вигляді рекурсивного визначення: ND=W (VND) на основі деяких множин імен V і значень W. Основними функціями над номінативними даними є наступні функції: іменування vD та розіменування vD із параметром v V, а також бінарні операції та предикати такі, як: об'єднання D, віднімання \D, рівність (=W)D на W. Визначається функція побудови порожнього номінативного даного D, предикат належності W: WD. Задана операція реномінації для номінативного даного ([a1b1, …, vbi, …])a1b1, …, xbi, …]. Основними композиціями функцій над номінативними даними є бінарні композиції: множення D , ітерації D, з'єднання D та тернарна композиція розгалуження D. Показано, що композиція множення відповідає послідовному застосуванню функцій, композиція розгалуження – умовному оператору if-then-else мов програмування, композиція ітерації D – оператору until-do, а композиція з'єднання D здійснює об'єднання номінативних даних, що є результатами функцій-аргументів.

Побудований клас номінативних даних дозволяє визначити досить багатий клас функцій, однак, ці функції не можуть працювати з динамічними даними, які вимагають обчислення нових імен. Для розв’язання цієї проблеми припускається, що деякі імена можуть іменувати інші імена (бути їх метаіменами). Це фактично означає, що імена можуть виступати як значення, тобто, що VW, клас даних з такою властивістю називається класом метаномінативних даних. Тому в підрозділі 2.5 до розгляду водяться метаномінативні дані, функції та композиції над ними. При цьому клас метаномінативних даних визначається, як , де W – деяка множина базових елементів (праелементів). Для обробки метаномінативних даних додаткового вводяться функція вибору імені компоненти D (d)=v, якщо vrnd, де v, dD та бінарні композиції присвоювання (іменування) asD, взяття значення (розіменування) cnD, які задаються наступним чином: asD(f, g)(d)=[f(d) g(d)] та cnD(f, g)(d)=k(d), якщо f(d) k(d) n g(d). Остання композиція є частковою багатозначною композицією.

Далі будемо вживається термін номінативні дані, маючи на увазі дані з класу MND.

Підрозділ 2.6 присвячений опису імперативних композиційно-номінативних систем (ІКНС), які задають спеціальну мову програмування. В ІКНС композиційна система CmS(Z) = <D, F, C> конкретизована таким чином, що D =MND – множина номінативних даних над W, FD – множина часткових багатозначних функцій (бінарних відношень) над MND, Z = Nat, C=D, D, D, D}. Параметри дескриптивної системи DsS(Z) = <FN, CN, Ds> конкретизовані як FN={0, 1,,W,\ , , =W, as, cn, } та CN={, , ,

Оскільки зі стандартними дескрипціями не завжди зручно працювати, індуктивно визначено нову множину дескрипцій (термів) TND:

1) 0, 1,,W,\ , , =W, as, cn, TND,

2) якщо t1, t2, t3 TND, то t1t2, (t1, t2, t3), t1t2 , t1t2 TND.

Тим самим побудована ІКНС задає деяку мову, яка може розглядатися як спеціальна мова програмування.

Підрозділ 2.7 присвячений опису предикатних композиційно-номінативних систем (ПКНС), які визначають спеціальну мову специфікацій програм. ПКНС задається введенням спеціальної композиційної системи PCS(Nat) = <D,P,C>, де D –-довільна не порожня множина даних, P=DBool –-множина предикатів, C множина n-арних композицій на P.

Визначено предикатну композиційну систему PCS = < XA, XA Bool, {K , K , R K , xK }>, дескриптивну систему DsS = <PN, {, , R, xStForm>, де PN – множина символів базових предикатів, а StForm – множина стандартних дескрипцій, яку звичайно називають множиною формул денотаційної системи DnS=<den_cn, den_fn>. Тим самим побудовано ПКНС <PCS, Ds, Dn>, яка називається системою першого порядку. Нас цікавить випадок такої системи при якому A конкретизується як клас номінативних даних, а PN конкретизуються як імена предикатів, що характеризують номінативні дані. У якості таких предикатів обрано предикати номінативної належності (n)D, рівності на класі номінативних даних =D і належності множині базових елементів WD. Останній предикат позначається символом U, щоб уникнути частого вживання символу . Таким чином, PN = {n, =, U}. Зазначена конкретизація визначила нову ПКНС, яка називається системою специфікації номінативних даних (СКНС). Ця система досліджується як у семантичному аспекті, так і в синтаксичному (аксіоматичному) аспекті. З цією метою змінено клас стандартних формул СКНС на клас традиційних формул мов першого порядку та побудовано спеціальну аксіоматичну теорію номінативних даних (ТМНД).

У третьому розділі “Обчислюваність функцій над номінативними даними”, враховуючи такі особливості програмування, як використання складних структур даних, частковість і недетермінованість програм, запропоновано:

транзитивні дані та натуральні числа;

натуральна обчислюваність над номінативними даними;

номінативна обчислюваність;

номінативна обчислюваність частково рекурсивних функцій (ЧРФ);

обчислюваність над транзитивними даними;

номінативна та натуральна обчислюваність функцій.

Традиційні визначення обчислюваності n-арних функцій, задані на натуральних числах або словах, не дозволяють адекватно задати обчислюваність над складними структурами даних. Тому необхідно уточнювати обчислюваність функцій над структурами даних, які дозволяють адекватно задати складні структури даних. Однією з таких структур є структура номінативних даних MND. Досліджено різні види обчислюваностей над номінативними даними. Також виконано порівняння виразної сили цих видів обчислюваності.

У підрозділі 3.1 визначено транзитивні дані та натуральні числа в запропонованій моделі номінативних даних. Досліджується множина транзитивних даних Trd, а також властивості на цій множині. Множина транзитивних даних є алгеброю з операціями додавання та множення. Нулем цієї алгебри виступає [(позначається ), а одиницею []. Множина транзитивних даних може розглядатися як множина скінченних ординалів, таким чином, показано можливість побудови множини натуральних чисел Nat в класі номінативних даних.

Для опису повного класу обчислюваних функцій над номінативними даними можна застосувати натуральну обчислюваність над номінативними даними, яка досліджується у підрозділі 3.2. Клас натурально обчислюваних функцій над номінативними даними відносно відношень натуралізації (nat) і денатуралізації (denat) позначається Cn(MND, nat, denat).

Така побудова натуральної обчислюваності дозволяє довести низку важливих властивостей натурально обчислюваних функцій. Натуральна обчислюваність орієнтована на традиційну систему обчислюваних функцій та композицій. Крім цього, вона прив'язана до функцій nat і denat, а також орієнтована на використання натуральних чисел для кодів і елементів послідовностей. Все це порушує адекватність задання повного класу обчислюваних програмних функцій.

Для більш адекватного опису повного класу обчислюваних функцій над номінативними даними у підрозділі 3.3 побудовано номінативну обчислюваність, яка базується на системі базових функцій та композицій, близьких до функцій та композицій, що застосовуються в мовах програмування. При цьому згідно з визначенням 3.3.1 номінативно обчислюваними називаються функції над MND, отримані замиканням функцій {0, 1, D, D, D, \D, (=W)D, asD, cnD,WD } відносно множини композицій { D, D, D, D}. Клас номінативно обчислюваних функцій позначено як Cmn(W).

У підрозділі 3.4 показано, що будь-яка ЧРФ може бути представлена номінативно обчислюваними функціями над множиною Nat у номінативних даних.

У підрозділі 3.5 побудовано спеціальний вид обчислюваності – обчислюваність над транзитивними даними, яка є аналогом натуральної обчислюваності, де множина Nat моделюється за допомогою множини транзитивних даних Trd, і відповідно замість функцій nat і denat використовує функції trdin і detrdin. У підрозділі 3.6 показано, що має місце теорема 3.6.1 яка стверджує, що для будь-якого W має місце Cns(W)=Cmn(W). Тобто, клас номінативно обчислюваних функцій при заданих стандартних функціях nat і denat збігається з класом натурально обчислюваних функцій. Для доведення цієї теореми показана номінативна обчислюваність функцій trdin і detrdin, а також, що між множинами Nat і Trd існує взаємно однозначна відповідність.

У четвертому розділі “Аксіоматичні системи для композиційно-номінативних мов специфікацій програм над номінативними даними”, досліджено наступні питання:

аксіоматизації теорії номінативних даних;

операції над номінативними даними;

поняття функції та відношення в теорії номінативних даних;

транзитивні дані та натуральні числа в теорії номінативних даних;

принципи -вибору, -виділення та -заміни в теорії номінативних даних;

представимість натурально обчислюваних функцій -предикатами;

неповнота теорії номінативних даних.

У підрозділі 4.1 розглянуто аксіоматизацію теорії номінативних даних. Теорія номінативних даних будується як аксіоматична теорія 1-го порядку з рівністю та тернарною зв’язкою (предикатом) номінативної належності, що записується в інфіксній формі xyna (або (x,y)na).

Природно, що при побудові аксіоматичної теорії номінативних даних можна спиратися на різні аксіоматики теорії множин. У роботі використано теорію допустимих множин, що має низку переваг: з одного боку, ця теорія досить потужна, щоб породжувати обчислювані функції над різними структурами даних, з іншого ж боку, вона не настільки обмежувальна, як різні варіанти конструктивних логік, але і не надмірно потужна та не допускає, наприклад, застосування аксіоми побудови множини всіх підмножин. Крім того, ця теорія використовує базові дані (праелементи), що відповідає методам побудови даних у програмуванні. Використовується унарний предикат U, істинний на елементах базової множини W. Іншими словами, розглядається структура <A, n, =, U>.

Класом 0-формул називається найменший клас Y, що містить елементарні формули і замкнений відносно наступних операцій: 1) якщо Y, то і Y, 2) якщо , Y, то і Y і Y, 3) якщо Y, то і xyna , xyna Y для всіх змінних x, y, a.

Клас -формул є найменший клас Z, що містить 0-формули і замкнений відносно умов 2) та 3) визначення класу 0-формул і наступної умови екзистенціальної квантифікації: якщо Z, то u Z.

Показано, що кожна номінативно обчислювана функція подається деяким бінарним - предикатом P(x,y), тобто f(x)=y тоді і тільки тоді, коли P(x,y). Для цього побудовано опис всіх функцій, зазначених у визначенні номінативної обчислюваності, а також всіх функцій, отриманих застосуванням композицій. Спеціальні аксіоми аксіоматичної системи специфікацій програм над НД поділено на три групи: перша група призначена для опису властивостей рівності, друга – для опису властивостей множини даних. Третя група аксіом представляє властивості НД:

екстенсіональність: x y (xyn a xyn b) a=b;

фундованість (індукція за належністю): (a(xyn a ( x) ( y) (a))) a (a);

індукція за включенням: (a(ba (b) (a))) a (a);

0-виділення: b x y (xyn b xyn a 0(a));

іменування: c xyn c;

об’єднання: c(ac bc);

нетривіальність: a xy (x yn a).

У підрозділі 4.2 досліджено операції над номінативними даними та доведені твердження: теорема 4.2.1 (про існування номінативного даного, яке містить елемент з заданим іменем), теорема 4.2.2 (про існування номінативного даного, яке містить заданий елемент), теорема 4.2.3 (про існування номінативного даного, яке містить тільки даний елемент), теорема 4.2.4 (про існування номінативного даного, яке містить тільки задану пару елементів), теорема 4.2.5 (про існування номінативного даного, яке містить задану пару елементів), теорема 4.2.6 (про існування множини двох елементів), лема 4.2.1 (про існування унікальної множини 0 без елементів).

Наведено визначення 4.2.1 номінативної множини a=x,y (u,v)na((u=xv=x)(u=yv=y)). А також показано, що мають місце наступні твердження: властивість 4.2.1 {x, x{x} та лема 4.2.2 xy!a(a={x, y

Для MND визначено різні відношення, зокрема: належніcть до ідентифікаторів (xida uvna(u=x)), належніcть до множини значень (xva uvna(v=x)), належніcть до множини компонент (xKa uvna((u=x)(v=x))). Відповідно до запропонованих відношень належності визначено відношення включення за ідентифікаторами, включення за значеннями, включення за компонентами, рівність за ідентифікаторами, рівність за значеннями, рівність за компонентами. Крім того, запропоновано бінарні операції об’єднання, перетину та віднімання та досліджено їх властивості.

Визначено 0-предикат set(a)(x, y)na (x=y), який задає властивість метаномінативної множини (МНМ) “бути множиною”.

У підрозділі 4.3 визначено поняття функції та відношеннь в теорії номінативних даних. Для цього, зокрема, визначено:

впорядковану пару елементів a=<x, y>(u,na((u=0v=x)(u=1v=y)),

декартовий добуток

с=ab(x, y)nc(x=y(u, v)na(z, t)nb(x=<[uv],zt]>))

((u, v)na(z, t)nb(x, y)nc(x=yx=<[uv],zt]>)),

впорядкований n-кортеж <x1, …, xn>=<x1, <x2, …, xn>>,

декартовий добуток n MND a1an= a1(a2an).

Досліджено властивості запропонованих структур даних.

Визначено предикати “a – впорядкована пара”, “a – впорядкована n-ка”, для довільного фіксованого n2, “a є відношенням”, що позначається Rel(a), “a є n-арним відношенням”, що позначається Reln(a), для довільного фіксованого n2.

Загальне поняття функції (необов’язково однозначної), заданої на MND, визначаєтся наступним чином: “f – функція”Rel(f).

Поняття однозначної функції, заданої на MND, визначається предикатом Fun(f): “f – однозначна функція”Fun(f)Rel(f)<x1,y1>nf <x2,y2>nf(x1=x2 y1=y2).

Задано область визначення Df та область значень Ef функції f , поняття n-арної функції та однозначної n-арної функції.

У підрозділі 4.4 досліджено транзитивні дані та натуральні числа в теорії номінативних даних. Визначено 0-предикати: a=succ(x)a=x[xx] та setr(a)set(a) xka (set(x) ukx (set(u) uka)), який задає властивість “бути транзитивною МНМ”.

Показані наступні властивості транзитивної МНМ множини: x!a(a=succ(x)), xkaxk succ(a), setr(x)setr(succ(x)), xy(x[xy]=), x(x[xx]=), xy((x, y)x), xy((y, x)x), x((x, x)x), xy(x[xy]), xy(x[yx]), x(x[xx]), x(xsucc(x)).

Наведено наступні визначення транзитивне дане trd, відношення “<”, “” та досліджено їх властивості.

Згідно з перерахованими властивостями, множина транзитивних даних є алгеброю з описаними операціями додавання і множення. Нулем цієї алгебри виступає , а одиницею []. Можна побудувати ізоморфізм алгебри транзитивних даних і натуральних чисел, тому, натуральні числа можна задати в класі номінативних даних. Показано, що мають місце наступні твердження: s(s=n), trd(n), тут n натуральне число. Визначено предикат nat, який формалізує поняття натурального числа в теорії метаномінативних множин (ТМНМ).

Введення натуральних чисел дозволило визначити послідовності seq(a) – дані вигляду (x0,..., xn)=[0x0,... n xn], та операції для роботи з ними: елемент послідовності s з індексом x: s[x]=y, довжина послідовності: ln(s)=n.

У підрозділі 4.5 розглянуті принципи -вибору, -виділення та -заміни в теорії номінативних даних.

У підрозділі 4.6 досліджено представимість натурально обчислюваних функцій -предикатами. Для цього побудовано подання всіх функцій, які зазначені у визначенні номінативної обчислюваності -предикатами. Тим самим доведена теорема 4.6.1: клас номінативно обчислюваних функцій реляційно представимий -предикатами ТМНД. Ця теорема свідчить про потужну виразну силу побудованої аксіоматичної системи номінативних даних.

У підрозділі 4.7 показано, що має місце неповнота теорії номінативних даних.

У п’ятому розділі, побудовано прототип реалізації аксіоматичної системи специфікацій програм над номінативними даними (NDSL), який базується на секвенційному численні композиційно-номінативних логік, та використовує синтаксичну нотацію близьку до мови специфікацій програм Z.

Система NDSL передбачає обробку тексту, написаного на описаній мові, яка полягає у виконанні наступних етапів: 1) переведення вхідного тексту в його внутрішнє представлення; 2) перевірка синтаксису; 3) перевірка типів; 4) перевірка несуперечливості специфікації; 5) перевірка властивостей.

Система пробує виводити кожну ціль від її попередників. Для цього, NDSL використовує вбудований прувер логік першого порядку, при цьому в якості аксіом система застосовує стандартні аксіоми, спеціальні аксіоми аксіоматичної системи специфікацій програм над НД, а також аксіоми зі схеми станів специфікації програми, тобто аксіоми, задані для кожної конкретної системи.

Продемонстровано, що система NDSL може доводити властивості програм. Тим самим показано, що застосований підхід може ефективно використовуватися для побудови аксіоматичної системи специфікацій програм над номінативними даними, що достатньо адекватно відповідає проблемам програмування.

Система NDSL написана на Borland JBuilder 2005 Foundation. Діаграма класів наведена в додатку А. Приклади застосування системи NDSL наведено в додатку Б.

Висновки

Головний результат дисертаційної роботи – розробка та дослідження композиційно-номінативних аксіоматичних систем для специфікацій програм, що орієнтовані на роботу зі структурованими даними, розв’язують практично важливі задачі специфікації програм та мають істотне значення для теорії і практики програмування.

В роботі запропоновано новий підхід до побудови аксіоматичних систем специфікацій програм над номінативними даними, в основі якого лежить композиційно-номінативний метод уточнення поняття програми. В результаті проведеної роботи:

побудовано клас моделей програм, що базуються на номінативних та, зокрема, метаномінативних типах даних;

визначено спеціальний вид обчислюваності – номінативну обчислюваність, яка базується на системі базових функцій і композицій, близьких до функцій та композицій мов програмування, та доведено співпадіння повного класу номінативно обчислюваних функцій з повним класом натурально обчислюваних функцій над номінативними даними;

доведено, що кожна частково рекурсивна функція може бути представлена номінативно обчислюваними функціями;

визначено та досліджено аксіоматичну теорію номінативних даних, яка дозволяє доводити низку важливих властивостей часткових багатозначних функцій (бінарних відношень);

побудовано прототип реалізації аксіоматичної системи специфікацій програм над номінативними даними, який базується на секвенційному численні композиційно-номінативних логік, використовує синтаксичну нотацію близьку до мови специфікацій програм Z та забезпечує доведення властивостей програм.

СПИСОК ОПУБЛІКОВАНИХ ПРАЦЬ

Омельчук Л.Л. Обчислюваність функцій над метаномінативними даними // Вісн. Київ. ун-ту. Сер.: фіз.-мат. науки. – 2001. – Вип.1. – С . .

Омельчук Л.Л. Секвенційне числення для композиційно-номінативних логік часткових предикатів // Вісн. Київ. ун-ту. Сер.: фіз.-мат. науки. – 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. – Koљice – Herѕany, Slovakia, 2006. P. 134-139.

Омельчук Л.Л. Система специфікацій програм над номінативними даними // Theoretical and applied aspects of program systems development (TAAPSD’2006). – Abstracts. – Kyiv, Ukraine, 2006. P. 96-100.

АНОТАЦІЇ

Омельчук Л.Л. Аксіоматичні системи cпецифікацій програм над номінативними даними. – Рукопис.

Дисертація на здобуття наукового ступеня кандидата фізико-математичних наук за спеціальністю 01.05.01 – теоретичні основи інформатики та кібернетики. – Київський національний університет імені Тараса Шевченка. – Київ 2007.

На основі композиційно-номінативного підходу побудовані та досліджені імперативні та декларативні моделі недетермінованих програм. Семантика таких програм задається частковими багатозначними функціями (бінарними відношеннями) над номінативними даними. Визначено повний клас натурально обчислюваних функцій такого типу та наведено його алгебраїчне подання. В роботі визначено спеціальний вид обчислюваності – номінативна обчислюваність. Номінативна обчислюваність дозволяє адекватно визначити повний клас обчислюваних функцій над номінативними даними. Номінативна обчислюваність орієнтована на функції і композиції, близькі до програмних функцій і композицій. Будується аксіоматична теорія номінативних даних, яка спроможна специфікувати усі номінативно обчислювані функції.

Побудовано прототип реалізації аксіоматичної системи специфікацій програм над номінативними даними, а також продемонстровано, що він дозволяє доводити деякі властивості програм.

Ключові слова: композиційне програмування, композиційно-номінативні системи, семантика програм, специфікація програмних систем, обчислюваність, частково обчислювані функції.

Омельчук Л.Л. Аксиоматические системы спецификаций программ над номинативными данными. – Рукопись.

Диссертация на соискание ученой степени кандидата физико-математических наук по специальности 01.05.01 – теоретические основания информатики и кибернетики. – Киевский национальный университет имени Тараса Шевченко. – Киев 2007.

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

На основании композиционно-номинативного подхода построены и исследованы императивные и декларативные модели недетерминированных программ. Семантика таких программ задана частичными многозначными функциями (бинарными отношениями) над номинативными данными. Определен полный класс натурально вычислимых функций такого типа и приводится его алгебраическое представление. В работе предложен специальный вид вычислимости – номинативная вычислимость, которая позволяет достаточно адекватно определить полный класс вычислимых функций над номинативными данными (НД). При этом номинативная вычислимость является инвариантной относительно множества праэлементов. Кроме этого, она ориентирована на функции и композиции, близкие к функциям и композициям, которые используются в языках программирования.

Определена и исследована теория номинативных данных (ТМНД), которая является достаточно богатой и способна специфицировать все номинативно вычислимые функции. Теория номинативных данных строится как аксиоматическая теория 1-го порядка с равенством и тернарной связкой (предикатом) номинативной принадлежности, которая записывается в инфиксной форме xyna (или (x,y)na).

Введены следующие важные классы формул:

Классом 0-формул называется наименьший класс Y, который содержит элементарные формулы и замкнут относительно следующих операций: 1) если Y, то и Y, 2) если , Y, то и Y и Y, 3) если Y, то и xyna , xyna Y для всех переменных x, y, a.

Класс -формул есть наименьший класс Z, который содержит 0-формулы, замкнут относительно условий 2) и 3) определения класса 0-формул и следующего условия экзистенциальной квантификации: если Z, то u Z.

Специальные аксиомы аксиоматической системы спецификаций программ над НД поделены на три группы: первая группа предназначена для описания свойств равенства, вторая группа – для описания свойств множества данных. Третья группа аксиом описывает свойства НД:

экстенсиональность: x y (xyn a xyn b) a=b;

фундированность: (a(xyn a ( x) ( y) (a))) a (a);

индукция по включению: (a(ba (b) (a))) a (a);

0-выделение: b x y (xyn b xyn a 0(a));

именование: c xyn c;

объединение: c(ac bc);

нетривиальность: a xy (x yn a).

Теория номинативных данных развивается аналогично теории допустимых множеств (С. Крипке, Р. Платек, Дж. Барвайз, Ю.Л. Ершов).

В диссертации показано, что каждая номинативно вычислимая функция представляется некоторым бинарным -предикатом. Для этого построены представления всех функций, упоминаемых в определении номинативной вычислимости, а также всех функций, получаемых применением композиций. Тем самым доказана теорема 4.6.1: класс номинативно вычислимых функций реляционно представим -предикатами ТМНД. Доказанная теорема свидетельствует о мощной выразительной силе построенной аксиоматической системы номинативных данных. Показано, что имеет место неполнота теории номинативных данных.

На основании предложенной аксиоматической теории номинативных данных строится специальный язык спецификаций программ.

Построен прототип реализации аксиоматической системы спецификаций программ над номинативными данными (NDSL), а также продемонстрировано, что он позволяет доказывать свойства программ.

Полученные результаты рассматривались на ряде международных конференций.

Ключевые слова: композиционное программирование, композиционно-номинативные системы, семантика программ, спецификация программных систем, вычислимость, частично вычислимые функции.

Omelchuk L.L. Axiomatic Systems of Specifications of Programs over Nominative Data. – Manuscript.

Thesis for awarding the degree of the candidate of Physics and Mathematics. Speciality 01.05.01 – Theoretical bases of computer science and cybernetics. – National Taras Schevchenko University of Kyiv. – Kyiv 2007.

Imperative and declarative models of nondeterministic programs based on composition-nominative approach are constructed and investigated. Semantics of such programs is presented by partial multi-valued functions. The complete class of naturally computable functions of described type is defined and its algebraic representation is built. A special computability considered in this paper is nominative computability. Nominative computability allows to set adequately a complete class of computable functions over nominative data. At the same time nominative computability is invariant relative to a set of basic elements. Moreover, it is oriented to functions and compositions, which are close to function and compositions of programming languages.

An axiomatic theory of nominative data, which is capable to specify all computable functions, is constructed.

A prototype of axiomatic system of specifications of programs over nominative data is constructed.

Keywords: composition programming, composition nominative systems, semantics of the programs, program system specification, computability, partially computable functions.