Верифікація перетворення між винятково функційною та імперативною предметно-орієнтованими мовами програмування на прикладі HELIX
Дата
2021
Автори
Зайчук Ілля Костянтинович
Назва журналу
ISSN журналу
Назва тому
Видавець
Анотація
HELIX є формально верифікованим ланцюжком мов програмування та правил перекладу, призначеним для генерації високоефективних імплементацій ряду чисельних алгоритмів. Будучи заснованим на існуючій системі SPIRAL, HELIX додає строгість формального доведення коректності з використанням інструменту інтерактивного доведення теорем Coq. Він формально описує набір предметно-орієнтованих мов, починаючи з HCOL, що задає абстрактний потік даних обчислення. Робота HELIX полягає в перетворенні початкової програми через низку проміжкових мов, що закінчується на LLVM IR.
В даній роботі описані три мови цього ланцюжка та формальна верифікація переходу між ними. Розглянуті переходи є нетривіальним, адже кожна наступна мова ланцюжка вводить абстракції нижчого рівня, у порівнянні з попередньою. Відбувається перехід від чисто функційної мови змішаного рівня вбудови до глибоко вбудованої імперативної, від абстрактного алгебраїчного типу даних до машинних чисел з рухомою комою, додається модель пам’яті, області видимості змінних та монадна обробка винятків. Продемонстрована архітектура цих мов, автоматичний перехід між ними та автоматизоване доведення збереження семантики на кожному з кроків.
Бібліографічний опис
Галузь знань та спеціальність
12 Інформаційні технології , 122 Комп’ютерні науки
Бібліографічний опис
Зайчук І. К. Верифікація перетворення між винятково функційною та імперативною предметно-орієнтованими мовами програмування на прикладі HELIX : дипломна робота ... бакалавра : 122 Комп’ютерні науки / Зайчук Ілля Костянтинович. - Київ, 2021. - 40 с.