Стендап Сьогодні 📢 Канал в Telegram @stendap_sogodni
🤖🚫 AI-free content. This post is 100% written by a human, as is everything on my blog. Enjoy!30.07.2023
Формальна верифікація: найслабкіша передумова
Після того, як отримали синтаксичне дерево програми, починається його обробка, а саме, як я писав на початку, створення теореми про вірність. Для цього використовується така модель як семантики перетворення предикатів.
Починаємо з післяумови, яка вже повинна бути задана. (До речі, я про це не згадав, але одна додаткова синтаксична функція моєї граматики — оголошення перед- та післяумов у коментарях.) Далі беремо останню команду та перетворюємо післяумову на найслабкішу передумову, яка гарантує справдження післяумови після цієї команди.
Розглянемо найпростіший приклад. Якщо команда — це присвоєння x = y+1, то всі згадки про x у післяумові треба замінити на y+1. Якщо післяумова була x > 0, то найслабкіша передумова - y+1 > 0.
Так рухаємось від останньої команди до першої, та послідовно перетворюємо умову. Перетворення для умовного оператора if лише трохи складніше та являє собою поєднання двох гілок. Перетворення для циклу суттєво складніше та потребує від нас оголошення інваріанта та обмеженої змінної. Інваріант — це умова, яка справджується після кожної ітерації циклу. Обмежена змінна — зобовʼязана зменшуватись з кожною ітерацією, але бути додатною. Ці анотації допомагають довести, що цикл закінчиться.
Нарешті, отримуємо найслабкішу передумову для всієї програми. Залишається тільки поєднати її з оголошеною передумовою знаком “випливає” (⇒) та теорема про вірність готова!
Мабуть, потрібно подумати про те, що така теорема стверджує. Вона обмежена тим змістом, який вклав програміст; без хорошої перед- та післяумови доведення не буде корисним — або навпаки, не буде можливим. У цьому формальна верифікація схожа на юніт-тести - “правильність” програми все одно залежить від людського розуміння. Різниця в тому, що юніт-тести перевіряють обмежений набір випадків, а формальна верифікація — буквально всі.