Верифікація перетворення між винятково функційною та імперативною предметно-орієнтованими мовами програмування на прикладі HELIX
Тип публікації :
Бакалаврська робота
Дата випуску :
2021
Автор(и) :
Зайчук Ілля Костянтинович
Мова основного тексту :
ua
eKNUTSHIR URL :
Цитування :
[APA 7] Зайчук, І. К. (2021). Верифікація перетворення між винятково функційною та імперативною предметно-орієнтованими мовами програмування на прикладі HELIX [Бакалаврська робота, Київський національний університет імені Тараса Шевченка]. eKNUTSHIR. https://ir.library.knu.ua/handle/123456789/3299
[ДСТУ] Зайчук І. К. Верифікація перетворення між винятково функційною та імперативною предметно-орієнтованими мовами програмування на прикладі HELIX : кваліфікаційна робота бакалавра : 12 Інформаційні технології. Київ, 2021. 40 с. URL: https://ir.library.knu.ua/handle/123456789/3299 (дата звернення: 25.07.2026).
HELIX є формально верифікованим ланцюжком мов програмування та правил перекладу, призначеним для генерації високоефективних імплементацій ряду чисельних алгоритмів. Будучи заснованим на існуючій системі SPIRAL, HELIX додає строгість формального доведення коректності з використанням інструменту інтерактивного доведення теорем Coq. Він формально описує набір предметно-орієнтованих мов, починаючи з HCOL, що задає абстрактний потік даних обчислення. Робота HELIX полягає в перетворенні початкової програми через низку проміжкових мов, що закінчується на LLVM IR.
В даній роботі описані три мови цього ланцюжка та формальна верифікація переходу між ними. Розглянуті переходи є нетривіальним, адже кожна наступна мова ланцюжка вводить абстракції нижчого рівня, у порівнянні з попередньою. Відбувається перехід від чисто функційної мови змішаного рівня вбудови до глибоко вбудованої імперативної, від абстрактного алгебраїчного типу даних до машинних чисел з рухомою комою, додається модель пам’яті, області видимості змінних та монадна обробка винятків. Продемонстрована архітектура цих мов, автоматичний перехід між ними та автоматизоване доведення збереження семантики на кожному з кроків.
В даній роботі описані три мови цього ланцюжка та формальна верифікація переходу між ними. Розглянуті переходи є нетривіальним, адже кожна наступна мова ланцюжка вводить абстракції нижчого рівня, у порівнянні з попередньою. Відбувається перехід від чисто функційної мови змішаного рівня вбудови до глибоко вбудованої імперативної, від абстрактного алгебраїчного типу даних до машинних чисел з рухомою комою, додається модель пам’яті, області видимості змінних та монадна обробка винятків. Продемонстрована архітектура цих мов, автоматичний перехід між ними та автоматизоване доведення збереження семантики на кожному з кроків.
Галузі знань та спеціальності :
12 Інформаційні технології
122 Комп’ютерні науки
Файл(и) :![Ескіз]()
Вантажиться...
Формат :
Adobe PDF
Розмір :
406.22 KB
Контрольна сума :
(MD5):6e88f59dcb8e04ac04f860284b44b1da
Якщо не вказано інше, ця робота розповсюджується на умовах ліцензії Creative Commons Attribution-NonCommercial 4.0 International