Главная

Мягкое введение в Coq: начало

2013-06-07 в 5:26, admin, рубрики: coq, формальная верификация, функциональное программирование, метки: coq, формальная верификация

Предисловие

Ни для кого не секрет, что ошибки в программах могут привести печальным последствиям. История знает множество случаев, когда переполнение счетчика или необработанное исключение приводило к большим материальным затратам и человеческим жертвам. Так, например, 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