Стендап Сьогодні 📢 Канал в Telegram @stendap_sogodni

🤖🚫 AI-free content. This post is 100% written by a human, as is everything on my blog. Enjoy!

28.07.2023

Вступ до формальної верифікації програм

Сьогодні піде мова про мою бакалаврську роботу — яка ставила собою засіб формальної верифікації програм на псевдо-JavaScript. Кінцевий результат реально працює, хоч і для академічно простих прикладів. Робота була написана на Clojure - бо я тоді від неї був в захваті — та стала цікавим досвідом функціонального програмування. Настільки цікавим, що пізніше я переписав її на F#, щоб випробувати й цю мову — до речі, мабуть, перше, що я робив з VSCode.

Що взагалі таке формальна верифікація? Просто кажучи, це як юніт-тести, але без виконання коду — тільки за статичним аналізом. Визначаєш початкові та кінцеві умови, а перевірка встановлює, що код при заданих початкових умовах в будь-якому разі прийде до кінцевих. От простий приклад.

Як можна досягнути такого результату? Насправді концептуально все просто. Раз — побудувати теорему про вірність — тобто, формальний вислів, який гарантує справдження післяумов. Два — довести теорему. Проблема в тому, що теорему довести складно навіть вручну, а автоматично — ще складніше. Детальніше — в наступні дні.

Чи має це все практичний сенс? Та взагалі має. Формальна верифікація остаточно доводить те, що програма працює правильно. Є мова SPARK - вона використовується для систем з високим ризиком — наприклад, авіоніки. Або середовище Coq. На жаль, через складність доведення теорем ваш додаток React навряд чи колись стане формально верифікованим.