Automation of formal verification of programs in the Pifagor language

В связи с увеличением сложности программного обеспечения корректность программы всё чаще доказывается с помощью методов формальной верификации. Дедуктивный анализ на основе исчисления Хоара применим для произвольных языков программирования и допускает частичную автоматизацию процесса. Однако дедуктивный анализ не нашёл широкого применения для верификации параллельных программ из-за высокой сложности процесса. Использование функционально-потоковой парадигмы параллельного программирования позволяет снизить сложность доказательства. В работе рассматривается процесс доказательства корректности функционально-потоковых параллельных программ на языке Пифагор и предлагается архитектура инструментального средства для поддержки процесса доказательства. Процесс доказательства корректности программы представляется в виде дерева, каждый узел которого — информационный граф программы, в котором дуги размечены формулами на языке спецификации. Корнем дерева является информационный граф программы с предусловием и постусловием, которые описывают ограничения на входные переменные и условия корректности результата работы программы соответственно. Основные преобразования, применимые к информационному графу программы: разметка дуг, эквивалентное преобразование, расщепление, свертка программы. Посредством данных преобразований информационный граф модифицируется и, в конечном счете, сводится к набору формул на языке спецификации, истинность которых будет свидетельствовать о корректности программы. Предложена архитектура системы поддержки процесса доказательства, которая позволяет строить дерево доказательства. В системе выделено несколько основных модулей: «Модуль доказательства корректности программы», «Система управления библиотекой аксиом и теорем» и «Модуль анализа ошибок и выдачи информации об ошибках». Согласно описанной архитектуре, разработано инструментальное средство для поддержки формальной верификации, которая позволяет строить дерево доказательства. Описана основная функциональность реализации системы.