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

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

Изменить 1

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

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

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

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

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

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

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

Ответ 1

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

Ответ 2

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

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

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

Ответ 3

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

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

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

Ответ 4

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

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

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

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

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

Валидация: "Мы пытаемся сделать правильные вещи?", то есть продукт, указанный для фактических потребностей пользователя?

Проверка: "Сделали ли мы то, что мы пытались сделать?", т.е. соответствует ли продукт спецификациям?

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

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

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

Ошибки времени выполнения (неизбежные ошибки, такие как ошибки ввода-вывода, обрабатываются, другие исключаются по дизайну).

нет непроизводительных бесконечных циклов.

Ответ 5

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