Стендап Сьогодні 📢 Канал в Telegram @stendap_sogodni
🤖🚫 AI-free content. This post is 100% written by a human, as is everything on my blog. Enjoy!31.07.2023
Формальна верифікація: доведення теореми
Коли в нас є теорема про вірність програми, залишається її довести. Що то взагалі значить — довести? В логіці теорема — це просто логічний вираз з невідомими. Довести — значить, показати, що для будь-якого набору значень невідомих теорема буде вірною. Як приклад: A || ~A (A або не A) буде вірним завжди, як можна побачити тривіально. На жаль, теореми про вірність виходять не такими простими. Тож як можна довести теорему — та ще й автоматичним шляхом?
Якщо невідомих небагато, можна довести повним перебором — тобто обчислити значення теореми для кожної комбінації та перевірити, що воно завжди буде істиною. Складність доведення росте експоненційно; для десяти невідомих це тривіально, для пʼятдесяти — нереально. (Кожний логічний вираз в програмі — рівність чи нерівність — стає невідомою в теоремі, та ще й деколи в різних варіаціях.) Я використовував такий метод до 20 невідомих.
А для складніших теорем я використовував метод резолюцій. Це підхід до доведення від оберненого: щоб довести нашу теорему, ми знаходимо підтвердження тому, що обернена теорема хибна. Для цього в оберненій теоремі треба знайти суперечність.
Пошук суперечностей відбувається за ітеративним алгоритмом. Спочатку теорему перетворюємо на конʼюнктивну нормальну форму — отримуємо, просто кажучи, ззовні AND, а всередині OR -дизʼюнкти. Достатньо знайти пару дизʼюнктів, які є протилежностями, щоб їхній AND ніколи не був істиною. Якщо з першої спроби не виходить - “схрещуємо” наявні дизʼюнкти, поки не знайдемо протилежні.
Буває й таке, що суперечність знайти неможливо — тоді теорема не буде доведеною, відповідно, вірність програми неможливо встановити. На жаль, остаточну відповідь “ні” ми не отримуємо — тільки відсутність успіху.