Rifat писал(а):
Предикатное программирование представляет собой рекурсивные функции и структуры данных .... В какой-то из ваших статей видел, что доказательство корректности проводится при помощи SMT солверов, то есть они умеют работать с рекурсивными функциями и умеют их доказывать.
Мне бы хотелось найти информацию, про то, как можно доказывать рекурсивные функции вручную. Можете подсказать какую-нибудь литературу про верификацию рекурсивных функций?
Прежде всего нужен метод доказательства корректности программы. Есть классический метод Хоара для императивных программ. У меня свой метод. На его базе построена система правил, применяемая при доказательстве корректности программы. Система правил расширена на случай рекурсивных вызовов с использованием меры. В основе этих правил -- классическая техника доказательства по индукции.
Доказывать корректность программы можно вручную или автоматически через инструмент автоматического доказательства. Не принципиально. Однако вручную можно ошибиться и пропустить ошибку в программе.
Статьи с доказательствами вручную закончились лет 15 назад. Вот одна из
классических работ.
Метод дедуктивной верификации предикатных программ описывается в
статье М.С.Чушкина. Примеры можно найти в
препринте.
Вход
FAQ
Поиск
