Стендап Сьогодні 📢 Канал в Telegram @stendap_sogodni
🤖🚫 AI-free content. This post is 100% written by a human, as is everything on my blog. Enjoy!29.07.2023
Формальна верифікація: обробка коду та граматики
З множини — єдність. Зараз на полях соняшник цвіте.
Будь-яка обробка коду, будь то компіляція, перевірка на вірність, форматування, або формальна верифікація, зазвичай починається з розбору на синтаксичне дерево. Так і тут. Для цього проєкту я обрав генератор парсерів ANTLR. Він видатний зокрема тим, що підтримує декілька мов — проміж них Java та C#. Для реалізації на Clojure я згенерував класи Java, а коли переписував на F# - то підійшла та сама граматика. Також ANTLR офіційно підтримує Golang та TypeScript. Одним словом, рекомендую мати у своєму арсеналі.
Граматику я писав з нуля. Спочатку намагався знайти готову, але це виявилося складно — бо те, що є, не підходило під мою семантичну модель. (Тут допомогла б стандартна модель esast, з системи Unified, але її ще не існувало.) На мою думку, для простих випадків граматику краще писати наново.
Граматика складається з правил для лексера та парсера. Лексер — розділяє текст на токени, тобто мінімальні значущі фрагменти. Правила лексера схожі на регулярні вирази. Токеном може бути ідентифікатор, число, дужка… Окремо визначаємося, що буде пробілами та незначущими символами. Це не тривіальне запитання — в одних мовах новий рядок розділяє команди, в інших — не має ніякого значення. В третіх мовах відступи мають значення. І так далі.
Правила парсера описують власне синтаксичне дерево. А саме, можливі варіанти того, як токени складаються у вузли дерева. Ну, наприклад: операція присвоєння: <ідентифікатор> <=> <вираз>. Найвищий вузол - програма: <команда>+, тобто програми складається з команд, а команди своєю чергою з виразів, а вирази з ідентифікаторів. Задача парсера — побудувати дерево, що відповідає тексту.
Коли синтаксичне дерево готове, можна перейти до побудови теореми про вірність.