Опыт дедуктивной верификации и синтеза программ

Обзор работ

Методы верификации и синтеза, предлагаемые в настоящей работе, базируются на концепции логической семантики и принципиально отличаются от классических методов верификации Флойда и Хоара [15, 16], определяющих построение формул частичной корректности императивных программ.

Наиболее популярным методом синтеза является извлечение программы из конструктивного (интуиционистского) доказательства (метод proofs-as-programs) [6] с применением правил резолюции и унификации. Синтез предикатных программ проводится в классической логике и, в соответствии с обзором [5], реализуется по шаблонам формул (метод schema-guided); в качестве шаблонов используются правила доказательства корректности. Метод шаблонов применяется в основном для синтеза логических программ. В работе [10] метод шаблонов применяется для синтеза императивных программ. В предикативном программировании Э. Хехнера [7] программа синтезируется как результат последовательных уточнений (refinements):

Q(x, y) Ü Q₁(x, y) Ü Q₂(x, y) Ü …

Ü Q_n(x, y) Ü LS(S)(x: y).

Однако вывод LS(S)(x: y) Þ Q(x, y) гарантирует лишь частичную корректность программы S. Данная формула – часть универсальной формулы корректности (2).

В работе [9] представлен синтез (методом proofs-as-programs) трех программ вычисления целочисленного квадратного корня применением трех разных схем доказательства по индукции теоремы тотальности: "x$m. Isqrt(x, m). В отличие от [9] метод синтеза, предлагаемый в настоящей работе, является универсальным и позволяет синтезировать произвольный алгоритм. Построение эффективного алгоритма вычисления целочисленного квадратного корня, модификации алгоритма sq3, описано в работе [8]. Исходная программа на языке Standard ML верифицирована автоматическим доказательством условий корректности в системе Nuprl. Конечная программа – результат серии оптимизирующих трансформаций, переводящих программу на язык HML, а затем на язык интегральных схем. Корректность трансформаций доказывается в Nuprl. Версия алгоритма в разделе 2 сопоставима с реализацией в [8]. Ее можно было бы оттранслировать на язык интегральных схем. Однако процесс построения программы в разделе 2 представлен на одном языковом уровне и значительно проще, чем в [8].

Первоначально каждая из трех стандартных функций была запрограммирована на языке P, причем для isqrt и ilog2 реализовано по три версии алгоритмов разной сложности и эффективности. Наиболее эффективные версии алгоритмов преобразованы на язык C++ применением оптимизирующих трансформаций. Итоговые программы для функций floor и isqrt оказались почти тождественными с исходными. Программа для функции ilog2 существенно быстрее исходной программы на C++.

Далее для каждой программы на языке P были сгенерированы условия корректности в соответствии с системой правил для однозначных спецификаций. Сгенерированные формулы оттранслированы на язык спецификаций известной системы автоматического доказательства PVS [4]. Доказательство на PVS оказалось нетривиальным и трудоемким процессом, требующим времени на порядок больше по сравнению с программированием без формальной верификации. Трудности возникали не столько при доказательстве самих условий корректности, сколько при доказательстве используемых математических свойств, особенно для битовой арифметики.

В процессе верификации обнаружено 5 ошибок. Из них четыре – чисто технические. Принципиальной является ошибка, обнаруженная для функции floor: результат функции floor для аргумента в формате 32 может не поместиться в формате 32. Это опасная ошибка, приводящая к неверным вычислениям.

Позднее в исследовательских целях был проведен программный синтез всех алгоритмов для трех функций. Оказалось, что в режиме синтеза процесс построения соответствующих теорий и логического вывода в системе PVS реализуется более естественным образом, более вариативно и с большей согласованностью между теориями. Это дает возможность сократить суммарный объем доказательств примерно в полтора раза по сравнению с режимом верификации. Работа в режиме синтеза оказывается более предпочтительной.

Методы верификации и синтеза, предлагаемые в настоящей статье, опробованы примерно для 20 небольших программ. Разработанный алгоритм генерации формул корректности специализирован для разных видов операторов языка P, что обеспечивает построение адекватного набора формул корректности практически идеальным образом. Узким местом дедуктивной верификации остается автоматическое доказательство формул корректности. Доказательство на PVS формул корректности оказалось сложным и требовало времени в 7-10 раз больше времени обычной разработки программы без формальной верификации. Разумеется, современные системы автоматического доказательства, такие как Z3 и CVC3, базирующиеся на мощных SMT-решателях, позволят ускорить процесс доказательства.

Представленные методы верификации и синтеза целесообразны для применения в приложениях с высокими требованиями к надежности и безопасности программ.

Пятый год в Новосибирском государственном университете читается курс по предикатному программированию. Издано учебное пособие [11], которое может быть также использовано для подготовки инженеров-верификаторов. Опыт преподавания курса показал, что сопутствующей нетривиальной задачей является обучение студентов методам формальной спецификации программ.

Список литературы

[1] Карнаухов Н.С., Першин Д.Ю., Шелехов В.И. Язык предикатного программирования P. — Новосибирск, 2009. – 44с. – (Препр. / ИСИ СО РАН; N 153).

[2] Shelekhov V. The language of calculus of computable predicates as a minimal kernel for functional languages // BULLETIN of the Novosibirsk Computing Center. Series: Computer Science. IIS Special Issue. – 2009. – 29(2009). – P.107-117.

[3] Шелехов В.И. Модель корректности программ на языке исчисления вычислимых предикатов. — Новосибирск, 2007. — 50с. — (Препр. / ИСИ СО РАН; N 145).

[4] PVS Specification and Verification System. – SRI International. – http://pvs.csl.sri.com/

[5] Basin D., DeVille Y., Flener P., Hamfelt A., and Nilsson J. Synthesis of programs in computational logic // LNCS, 3049. ¾ P.30 – 65, 2004.

[6] Sorensen M.H., Urzyczyn P. Lectures on the Curry-Howard Isomorphism. — 2006. — 457 p.

[7] E.C.R.Hehner. A Practical Theory of Programming, second edition. – 2004. –

http://www.cs.toronto.edu/~hehner/aPToP/

[8] O'Leary J., Leeser M., Hickey J., Aagaard M. Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization. // Theorem Provers in Circuit Design, 1994 – P.52-71.

[9] Creitz C. Derivation of a fast integer square root algorithm. – 2003. –

http://www.nuprl.org/Algorithms/03cucs-intsqrt.pdf.

[10] Srivastava S., Gulwani S., and Foster J. From Program Verification to Program Synthesis. –POPL, 2010. – P. 313-326.

[11] Шелехов В.И. Предикатное программирование. Учебное пособие. — НГУ, Новосибирск, 2009. — 109с.

[12] Souris J., Wiels V. Delmas D. and Delseny H. Formal Verification of Avionics Software Products // LNCS, 5850. – P.532 – 546, 2009.

[13] O'Halloran C. Guess and Verify – Back to the Future // LNCS, 5850. – P.23 – 32, 2009.

[14] Ball T., Hackett B., Lahiri S., Qadeer S. and Vanegue J. Towards scalable modular checking of user-defined properties // LNCS, 6217. – P.1 – 24, 2010.

[15] C. A. R. Hoare. An axiomatic basis for computer programming // Communications of the ACM, 12(10). – P. 576 – 580, 1969.

[16] Floyd R. Assigning meanings to programs // Mathematical Aspects of Computer Science. – P. 19–32, 1967.

[17] Cohen E., Dahlweid M., Hillebrand M., Leinenbach D., Moskal M., Santen T., Schulte W., Tobies S. VCC: A Practical System for Verifying Concurrent C // LNCS, 5674, P. 1–22. 2009.

[18] Ануреев И.С., Марьясов И.В., Непомнящий В.А. Верификация C-программ на основе смешанной аксиоматической семантики // Моделирование и анализ информационных систем, Ярославский государственный университет, т. 17, № 3, 2010, c. 5-28.

[1] «математик-верификатор» было бы, возможно, более подходящим переводом для «verifiсation engineer»

[2] экспертная оценка автора

[3] Здесь и далее термин "корректность"используется в смысле тотальной корректности

[4] Однозначность спецификации следует из ее тотальности и формулы (3). Доказана однозначность программы при условии, что все используемые базисные операции являются однозначными

[5] Истинность правил определяется как истинность формул, получающихся заменой ├ на Þ.

[6] Из стандарта не очевидно, что floor(-0)=0.

Дата добавления: 2015-06-27