Пользователь
0,0
рейтинг
7 июня 2013 в 09:26

Разработка → Мягкое введение в Coq: начало tutorial

Предисловие


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

image

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

Третий способ заключается в экстракции определения в какой-нибудь язык программирования (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

Заключение


В следующих частях рассмотрим способы определения рекурсивных функций и работу с основными тактиками доказательств.

Рекомендуемая литература:
  1. Software Foundations
  2. Certified Programming with Dependent Types


Следующая часть.
Александр @ymn
карма
14,0
рейтинг 0,0
Реклама помогает поддерживать и развивать наши сервисы

Подробнее
Спецпроект

Самое читаемое Разработка

Комментарии (13)

  • +3
    А как верифицировать программы, написанные для Coq? Т.к. они пишутся людьми, в них же тоже возможны ошибки, которые нужно исключить?
    • 0
      Дело в том, что при формальной верификации доказывается соответствие программы ее формальному описанию. Если программа содержит ошибки, то это сразу станет ясно. Если же формальное описание отсутствует или содержит ошибки, то смысл верификации программы пропадает. Или я не правильно понял ваш вопрос?
      • +2
        Формальное описание — это же и есть программа для Coq, верно? Если в формальном описании есть ошибки, то смысл верификации программы пропадает — но как гарантировать то, что их нет? Иными словами, кто будет проверять проверяющего? :)

        Честно говоря, я пошел читать про формальную верификацию в Википедии и окончательно запутался в том, что же она, собственно, из себя представляет и как ее применить применительно к более «бытовым» сценариям. Вы не могли бы, например, в следующих статьях (или в комментариях, если ответ тривиален) показать, как именно можно верифицировать стандартный C-шный Hello World?

        #include <stdio.h>
        
        int main(int argc, char *argv[]) {
            printf("Hello, world!\n");
            
            return 0;
        }
        
        • 0
          Конечно, я к этому и веду потихонечку. Сначала надо рассказать про некоторые основы.
          • 0
            Тогда ждем следующих частей, спасибо.
        • +1
          Есть надежда на то, что формальное описание проще для понимания (так как декларативно), а может быть ещё и короче.
          К примеру, есть верифицированный компилятор C на Coq. В принципе, там могут быть ошибки, они и в самом стандарте могут быть.
    • 0
      То, что вы называете «программами для Coq» — это не программы, а доказательства, записанные на языке Coq. Coq — не язык программирования. Доказательство на Coq нельзя исполнить, но его можно проверить. Проверить при помощи, собственно, Coq, или, что то же самое, чекера (checker) Coq. Т. е. Coq (он же Coq checker) — это такая программа, которая проверяет доказательство, записанное на языке Coq. Единственное назначение доказательства на Coq — это быть пропущенным через Coq checker.

      На практике при записи доказательства на формальном языке (таком как Coq) в IDE (хоть Coq и не язык программирования, но среда для удобной интерактивной записи доказательств на Coq называется IDE) checker обычно постоянно запущен в процессе записи доказательства. Не знаю, как конкретно обстоят дела в Coq, но у меня в Isabelle/HOL (ещё один язык для записи доказательств) процесс происходит так: я набираю доказательство на Isabelle/HOL в специальном IDE, checker при этом всегда запущен в фоне, и если что-то не так, проблемное место подчёркивается красным.

      Видимо, это и имел в виду ymn, когда написал в посте выше «Если программа содержит ошибки, то это сразу станет ясно». Т. е. если исходная программа на каком-нибудь языке программирования (C, OCaml, Scheme, Haskell) содержит ошибки, то при попытке записи формального доказательства (на языке Coq) её правильности, IDE «подчеркнёт проблемные места красненьким».

      Формальное описание — это же и есть программа для Coq, верно?


      Нет. Есть три «штуки»:
      1. Исходная программа (на C или любом другом языке программирования, которую мы хотим проверить).
      2. Спецификация этой программы, написанная на формальном языке Coq, или, что то же самое, формальное описание исходной программы (а лучше даже сказать не «формальное описание программы», а «формальное описание задачи, которую программа должна решать»). Т. е. на формальном языке записываем, что «программа должна делать то-то и то-то». Т. е. формулировка математической теоремы о том, что программа соответствует своим требованиям, т. е. математическая формулировка требований к программе.
      3. Собственно, доказательство того, что программа правильная, т. е. доказательство упомянутой выше теоремы, т. е. доказательство того, что программа соостветствует своим требованиям, своему формальному описанию, т. е. спецификации.

      Упомянутое вами «формальное описание» — это пункт 2, а то, что вы называете «программой на Coq» — это пункт 3.

      Никакой проблемы курицы и яйца тут не возникает. Т. е. не нужно думать, что мы проверяем одну программу другой, её — третьей и т. д. Нет. Есть исходная программа (1). Мы пишем формальное доказательство (3) того, что она соответствует своим требованиям (2). Это доказательство (3) проверяется Coq'ом. И, собственно, всё. Стоп. Никакой дальше бесконечной рекурсии нет. Единственное, в чём тут можно усомниться — это в том, что сам checker Coq действительно правильный, и что проверка доказательства (3) Coq'ом действительно гарантирует его правильность
  • +1
    Язык ГАЛИНА придумали в институте ИРИНА…
  • +1
    Coq — очень крутая и интересная штука. Сам очень люблю подоказывать чего-нибудь, поломать голову. После него Haskell кажется детской игрушкой. Единственный недостаток, найти ему промышленное применение очень сложно. Я периодически поглядываю вакансии, не требуется ли кому-нибудь coq-программист, и пока ничего не нашел, к сожалению.
    • 0
      Просто Coq-программист скорее всего никому не нужен. Нужны специалисты со знанием предметной области. Например, если вы знаете Verilog/VHDL, то можно попробовать устроиться в Intel или Altera. Если же вы специалист в криптографии, то можно попробовать пробиться в исследовательские лаборатории при зарубежных институтах.
      • 0
        Похоже, что так и есть. Вроде даже видел какие-то вакансии, связанные с Verilog/VHDL, где-то в Питере. На сколько я понял, это что-то связанное с проектированием микроконтроллеров и доказательство их корректной работы. Конечно, хотелось бы работать с чем-то более высокоуровневым.
  • +2
    По первой статье сложно получить какое-либо впечатление о языке и его возможностях практического применения. Пока я вижу только
    enum day {Sunday, Monday, Tuesday, Wednesday, Thursday, Friday, Saturday};
    
    static const day NEXT_WEEKDAY[] = {Monday, Tuesday, Wednesday, Thursday, Friday, Monday, Monday};
    
    day next_weekday(day d) { return NEXT_WEEKDAY[d]; }
    
    ASSERT_EQ(Tuesday, next_weekday(next_weekday(Saturday)));
    
  • НЛО прилетело и опубликовало эту надпись здесь

Только зарегистрированные пользователи могут оставлять комментарии. Войдите, пожалуйста.