Генерация и доказательство формул корректности предикатных программ

Abstract

Парадигма предикатного программирования занимает промежуточное положение между парадигмами функционального и императивного программирования. Язык предикатного программирования P определяет класс программ, не взаимодействующих с внешним окружением. Эти программы реализуют функции, отображающие значения входных переменных в значения результатов и не взаимодействуют с внешним окружением. Метод дедуктивной верификации, используемый в предикатном программировании, существенно отличается от классических методов Флойда и Хоара. Он базируется на понятии логики программы. Метод позволяет доказывать тотальную корректность программ. Целью работы является разработка и реализация системы верификации программ на языке P. Система верификации состоит из трех компонент. Основной компонентой системы верификации является генератор формул корректности программы. Генератор реализует метод дедуктивной верификации предикатных программ. Две другие компоненты – это трансляторы на язык CVC3 и PVS. Сгенерированные формулы проходят проверку на истинность в SMT-решателе CVC3. Формулы, которые решатель не смог проверить, доказываются в системы PVS. В рамках работы была построена система правил вывода условий корректности. Реализована система дедуктивной верификации предикатных программ. Система успешно прошла апробацию в рамках курса “Формальные методы в описании языков и систем программирования”. Работа докладывалась на международной научной студенческой конференции 2014 года, где была удостоена диплома третьей степени. Объем работы составляет 62 страницы. В работе использовано 12 иллюстраций и 4 таблицы. В работе присутствуют ссылки на 24 внешних источника.