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

17

Я вижу пару различных исследовательских групп и, по крайней мере, одну книгу, в которой рассказывается об использовании Coq для разработки сертифицированных программ. Существует ли консенсус относительно того, что такое определение сертифицированной программы ? Из того, что я могу сказать, все это на самом деле означает, что программа была доказана общей и введите правильный. Теперь тип программы может быть чем-то действительно экзотичным, например, списком с доказательством того, что он непусто, отсортирован со всеми элементами & gt; = 5 и т. Д. Однако в конечном итоге это сертифицированная программа, только одна из которых показывает Coq, является суммой и типом где все интересные вопросы сводятся к тому, что было включено в окончательный тип?

Изменить 1

Основываясь на ответе wjedynak, я взглянул на статью Ксавьера Лероя «Формальная проверка реалистического компилятора», которая приведена в ответах ниже. Я думаю, что это содержит некоторую хорошую информацию, но я думаю, что более информативную информацию в этой последовательности исследований можно найти в статье Механизированная семантика для подмножества C-языка языка C Сандрин Блази и Ксавьер Лерой. Это язык, на который добавлена ​​оптимизация «Формальная проверка». В нем Blazy и Leroy представляют синтаксис и семантику языка Clight, а затем обсуждают валидацию этой семантики в разделе 5. В разделе 5 приведен список различных стратегий, используемых для проверки компилятора, что в некотором смысле дает обзор различных стратегий создания сертифицированной программы . Это:

  1. Обзор руководства
  2. Доказательные свойства семантики
  3. Проверенные переводы
  4. Тестирование исполняемой семантики
  5. Эквивалентность с альтернативной семантикой

В любом случае, возможно, есть моменты, которые могут быть добавлены, и мне бы хотелось услышать больше.

Возвращаясь к моему первоначальному вопросу о том, какое определение имеет сертифицированная программа, мне все еще немного неясно. Ответ Wjedynak дает ответ, но на самом деле работа Лероя включала создание компилятора в Coq, а затем, в некотором смысле, его удостоверение. Теоретически это позволяет теперь доказывать вещи о программах на С, так как теперь мы можем перейти на C- & gt; Coq-gt. В этом смысле кажется, что есть этот поток работы, где мы могли

  1. Напишите программу на языке X
  2. Форма модели программы с шага 1 в Coq или какой-либо другой инструмент помощника доказательства. Это может быть связано с созданием модели языка программирования в Coq или может потребовать непосредственного создания модели программы (т. Е. Перезаписи самой программы в Coq).
  3. Докажите некоторое свойство о модели. Возможно, это доказательство ценности. Может быть, это доказательство эквивалентности утверждений (такие вещи, как 3 = 1 + 2 или f (x, y) = f (y, x), что угодно.)
  4. Затем, основываясь на этих доказательствах, вызовите сертифицированную исходную программу.

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

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

    
задан wyer33 23.01.2014 в 22:54
источник
  • Вы поднимаете очень правильный вопрос. Если вы доказали, что результат функции всегда нечетный, значит, это уже означает, что эта функция верна? Наверное, нет. Из того, что я знаю, спецификации не описывают каждый аспект проблемы до последнего бита. Это означает, что правильнее сказать, что только «некоторые из аспектов верны». Кто-нибудь возразит? –  Kirill Kobelev 27.01.2014 в 21:56

5 ответов

6

Я согласен с тем, что понятие кажется смутным, но, по моему мнению, сертифицированная программа - это программа, оборудованная / вместе с доказательством правильности. Теперь, используя богатые и выразительные типы подписей, вы можете сделать так, что нет необходимости в отдельном доказательстве, но это часто бывает только вопросом удобства. Реальная проблема заключается в том, что мы подразумеваем под правильностью: это вопрос спецификации. Вы можете посмотреть, например. Ксавье Лерой. Формальная проверка реалистичного компилятора .

    
ответ дан wjedynak 24.01.2014 в 16:58
4

Прежде всего обратите внимание на то, что фраза «сертифицированная» имеет слегка французскую предвзятость: в другом месте часто используется выражение «проверено» или «проверено».

В любом случае важно спросить, что это на самом деле означает. X. Leroy и CompCert - очень хорошая отправная точка: это большой проект по проверке компилятора C, и Лерой всегда стремится объяснить своей аудитории, почему имеет значение проверка. Особенно, когда вы разговариваете с людьми из «сертификационных агентств», которые обычно означают тестирование, не доказывая.

Еще один большой проект проверки - L4.verified , в котором используется Isabelle / HOL. Эта часть изложения немного объясняет, что на самом деле заявлено и доказано, и что последствия. К сожалению, фактическое доказательство совершенно секретно, поэтому его нельзя проверить публично.

    
ответ дан Makarius 02.02.2014 в 23:17
  • Совершенно секретно? На веб-сайте, к которому вы привязаны, я могу прочитать «seL4, его доказательства, а также библиотеки и инструменты пользовательского пространства - это программное обеспечение с открытым исходным кодом, и к ним можно получить доступ из seL4.systems». –  Zimm i48 14.08.2017 в 12:51
2

Сертифицированная программа - это программа, которая сопряжена с доказательством того, что программа удовлетворяет ее спецификации, то есть сертификату. Ключ состоит в том, что существует доказательный объект, который может быть проверен независимо от инструмента, создавшего доказательство.

Проверенная программа прошла проверку, которая в этом контексте может обычно означать, что ее спецификация была формализована и доказана правильно в такой системе, как Coq, но доказательство не обязательно сертифицировано внешним инструментом.

Это различие хорошо подтверждено в научной литературе и не является специфическим для франкофонов. Xavier Leroy очень четко описывает это в Разделе 2.2 Формально подтвержденный компилятор back-end .     

ответ дан Rob Blanco 02.08.2017 в 17:30
1

Я понимаю, что «сертифицированный» в этом смысле как указал Макарий , английское слово, выбранное франкоязычными людьми, где говорящие могли бы вместо этого использовать «официально подтвержденный». Coq был разработан во Франции и имеет множество франкоязычных разработчиков и пользователей.

Что касается того, что означает «формальная проверка», Wikipedia примечания (лицензия : CC BY-SA 3.0 ), что он:

  

- это акт доказательства ... правильности намеченных алгоритмов, лежащих в основе системы в отношении определенной формальной спецификации или свойства, с использованием формальных методов математики.

(Я понимаю, что вы хотели бы получить гораздо более точное определение, чем это. Надеюсь, что в будущем я буду обновлять этот ответ, если найду его.)

Википедия особенно отмечает разницу между проверкой и валидацией :

  
  • Проверка: «Мы пытаемся сделать правильные вещи?», то есть продукт, указанный для фактических потребностей пользователя?
  •   
  • Проверка: «Сделали ли мы то, что мы пытались сделать?», т. е. соответствует ли продукт спецификациям?
  •   

ориентир документ seL4: формальная проверка ядра ОС (Klein, et al., 2009) подтверждает эту интерпретацию:

  

Циник может сказать, что доказательство реализации показывает, что   реализация имеет точно такие же ошибки, что и спецификация   содержит. Это верно: доказательство не гарантирует, что   спецификация описывает поведение, которое пользователь ожидает.   разница [в проверенном подходе по сравнению с не проверенным]   это степень абстракции и отсутствие целых классов ошибок.

Какие классы ошибок есть? Учебник Agda дает некоторое представление :

  
  • Ошибки времени выполнения (неизбежные ошибки, такие как ошибки ввода-вывода, обрабатываются, другие исключаются по дизайну).
  •   
  • нет непроизводительных бесконечных циклов.
  •   
    
ответ дан sampablokuper 01.08.2017 в 22:47
0

Это может означать отсутствие ошибок во время выполнения (числовое переполнение, недопустимые ссылки ...), что уже хорошо по сравнению с большинством разработанных программных продуктов, хотя и остается слабым. Другое значение доказывается как правильное в соответствии с формализацией домена; то есть он должен не только быть формально свободным от ошибок во время выполнения, но также необходимо доказать, что он должен делать (что должно быть точно определено).

    
ответ дан Hibou57 20.04.2014 в 05:33