Предисловие
Ни для кого не секрет, что ошибки в программах могут привести печальным последствиям. История знает множество случаев, когда переполнение счетчика или необработанное исключение приводило к большим материальным затратам и человеческим жертвам. Так, например, 4 июня 1996 года европейская ракета-носитель «Ariane 5» буквально развалилась на части на 39-й секунде полета. Анализ инцидента показал, что авария произошла из-за ошибки в программном обеспечении. Ущерб составил около $7 млрд. В феврале 1991 года ракета «Patriot» промахнулась мимо цели из-за ошибки округления, успела пролететь лишние 500 метров. Ущерб: 28 убитых и более сотни раненых. Подобного рода ошибки встречаются и в аппаратном обеспечении. Недавний баг в процессорах Pentium, связанный с неправильным делением чисел с плавающей точкой, вынудил Intel пойти на замену бракованных чипов. Эта ошибка стоила компании $475 млн.
При проектировании аппаратного обеспечения или программ с повышенными требованиями к надежности широко используют формальную верификацию – формальное доказательство соответствия предмета верификации его формальному описанию. Предметом здесь могут являться алгоритмы, цифровые схемы, HDL описания аппаратуры и т. п.
Процедура формальной верификации – это довольно долгое и рутинное занятие. Поэтому оно оправдано далеко не во всех случаях. Для повседневных приложений подойдет и обычное тестирование. Здесь надо понимать, что тестирование не может доказать отсутствие в программе ошибок и ее соответствие формальному описанию.
Разумеется далеко не все утверждения можно доказать автоматически. В таких случаях на помощь приходят системы проверки доказательств (proof checker, proof assistant), одной из которых является Coq.
Введение
Coq – это интерактивная оболочка для доказательства теорем, в которой используется собственный функциональный язык программирования с зависимыми типами – Gallina. Его придумали и реализовали сотрудники французского института INRIA в середине 80-х годов. В настоящее время Coq доступен для GNU/Linux, Windows и MacOS. Исходные коды распространяются на условиях лицензии LGPL v.2.
Для работать с Coq можно несколькими способами: в консоли в интерактивном режиме, в графическом режиме в CoqIDE или в Emacs с помощью плагина Proof General.
Итак, Coq установлен и готов к работе. Попробуем что-нибудь написать!
В языке Coq нет никаких встроенных батареек – ни логических значений, ни чисел (на самом деле существует стандартная библиотека со множеством полезных определений и лемм, но в академических целях будем считать, что этого ничего нет). Вместо этого Coq предоставляет мощные средства для определения новых типов данных и функций, которые оперируют и трансформируют эти типы. Рассмотрим конкретный пример:
Inductive day : Type := | monday : day | tuesday : day | wednesday : day | thursday : day | friday : day | saturday : day | sunday : day.
Этим объявлением мы говорим Coq, что хотим определить новый набор значений данных – тип. Этот тип носит имя
day, а значения этого типа – monday, tuesday и т. д. Теперь мы можем написать функцию над значениями типа day. Напишем функцию, вычисляющую следующий рабочий день:Definition next_weekday (d:day) : day := match d with | monday => tuesday | tuesday => wednesday | wednesday => thursday | thursday => friday | friday => monday | saturday => monday | sunday => monday end.
В Coq есть вывод типов, сопоставление с образцом и прочие вещи, свойственные функциональным языкам программирования.
После того, как мы определили функцию, самое время проверить ее работоспособность на нескольких примерах. Во-первых, мы можем использовать команду
Eval simpl:Eval simpl in (next_weekday friday). (* ==> monday : day *) Eval simpl in (next_weekday (next_weekday saturday)). (* ==> tuesday : day *)
Во-вторых, мы можем явно указать ожидаемый результат и поручить Coq проверить его:
Example test_next_weekday: (next_weekday (next_weekday saturday)) = tuesday. Proof. simpl. reflexivity. Qed.
При работе в CoqIDE удобно пользоваться пошаговым выполнением программы, чтобы увидеть промежуточные результаты:
Третий способ заключается в экстракции определения в какой-нибудь язык программирования (OCaml, Scheme или Haskell). Это одна из основных фич системы Coq, ради которой все и разрабатывалось:
Extraction Language Ocaml. Extraction "/tmp/day.ml" next_weekday.
Вот что получилось в результате экстракции нашей функции в OCaml:
type day = | Monday | Tuesday | Wednesday | Thursday | Friday | Saturday | Sunday (** val next_weekday : day -> day **) let next_weekday = function | Monday -> Tuesday | Tuesday -> Wednesday | Wednesday -> Thursday | Thursday -> Friday | _ -> Monday
Заключение
В следующих частях рассмотрим способы определения рекурсивных функций и работу с основными тактиками доказательств.
Рекомендуемая литература:
Следующая часть.
