Побудова та дослідження програмних логік

У дисертаційній роботі введено композиції Флойда-Хоара та побудови умови за прообразом для програмних алгебр часткових квазіарних предикатів та функцій. Доведено їх монотонність та неперервність. На основі отриманих програмних алгебр побудовано програмні логіки для простих номінативних даних, складних ієрархічних номінативних даних та типізованих простих номінативних даних. Досліджено повноту та коректність класичної аксіоматичної системи логіки Флойда-Хоара для зазначених програмних логік, обґрунтовано необхідність побудови коректних аксіоматичних систем за допомогою введення додаткових обмежень на правила виводу. Розглянуто випадки коректних аксіоматичних систем з простими додатковими обмеженнями та обмеженнями, що базуються на властивостях правил виводу, для них досліджено питання повноти та коректності.

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

Криволап А. В. Побудова та дослідження програмних логік : дис. ... канд. фіз.-мат. наук. : 01.05.01 Теоретичні основи інформатики та кібернетики / Криволап Андрій Володимирович. - Київ, 2016. - 130 с.