Побудова та дослідження програмних логік
Тип публікації :
Дисертація
Дата випуску :
2016
Автор(и) :
Криволап Андрій Володимирович
Науковий(і) керівник(и)/редактор(и) :
Нікітченко Микола Степанович
Мова основного тексту :
ua
eKNUTSHIR URL :
Цитування :
[APA 7] Криволап, А. В. (2016). Побудова та дослідження програмних логік [Дис. канд. фіз.-мат. наук., Київський національний університет імені Тараса Шевченка]. eKNUTSHIR. https://ir.library.knu.ua/handle/123456789/7153
[ДСТУ] Криволап А. В. Побудова та дослідження програмних логік : дис. … канд. фіз.-мат. наук. : 11 Математика та статистика. Київ, 2016. 130 с. URL: https://ir.library.knu.ua/handle/123456789/7153 (дата звернення: 25.07.2026).
У дисертаційній роботі введено композиції Флойда-Хоара та побудови умови за прообразом для програмних алгебр часткових квазіарних предикатів та функцій. Доведено їх монотонність та неперервність. На основі отриманих програмних алгебр побудовано програмні логіки для простих номінативних даних, складних ієрархічних номінативних даних та типізованих простих номінативних даних. Досліджено повноту та коректність класичної аксіоматичної системи логіки Флойда-Хоара для зазначених програмних логік, обґрунтовано необхідність побудови коректних аксіоматичних систем за допомогою введення додаткових обмежень на правила виводу. Розглянуто випадки коректних аксіоматичних систем з простими додатковими обмеженнями та обмеженнями, що базуються на властивостях правил виводу, для них досліджено питання повноти та коректності.
Ключові слова: верифікація, композиційно-номінативний підхід, аксіоматичні системи, повнота та коректність, ієрархічні дані, типізовані дані.
Ключові слова: верифікація, композиційно-номінативний підхід, аксіоматичні системи, повнота та коректність, ієрархічні дані, типізовані дані.
Галузі знань та спеціальності :
11 Математика та статистика
111 Математика
Файл(и) :![Ескіз]()
Вантажиться...
Формат :
Adobe PDF
Розмір :
2.53 MB
Контрольна сума :
(MD5):be3800dbdd5e562de42b66d38bba235f
Якщо не вказано інше, ця робота розповсюджується на умовах ліцензії Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International