Формальная проверка программы на практике

66

Как инженер-программист, я пишу много кода для промышленных продуктов. Относительно сложные вещи с классами, потоками, некоторыми проектными усилиями, но также и некоторыми компромиссами для производительности. Я много тестирую, и я устал от тестирования, поэтому я заинтересовался инструментами формального доказательства, такими как Coq, Isabelle ... Могу ли я использовать один из них, чтобы формально доказать, что мой код не содержит ошибок, и все готово? с этим? - но каждый раз, когда я проверяю один из этих инструментов, я не уверен, что они пригодны для повседневной разработки программного обеспечения. Теперь это может быть только я, и я ищу указатели / мнения / идеи по этому поводу :-)

В частности, у меня складывается впечатление, что для того, чтобы заставить один из этих инструментов работать на меня, потребовались бы огромные инвестиции, чтобы правильно определить, проверять объекты, методы ... рассматриваемой программы. Затем я задаюсь вопросом, не исчерпает ли прувер пар, учитывая размер всего, с чем ему придется иметь дело. Или, может быть, мне придется избавиться от побочных эффектов (эти средства проверки, кажется, действительно хорошо работают с декларативными языками), и мне интересно, приведет ли это к «проверенному коду», который нельзя будет использовать, потому что он не будет быстрым или достаточно небольшой. Кроме того, я не могу позволить себе роскошь менять язык, с которым я работаю, это должен быть Java или C ++: я не могу сказать своему боссу, что с этого момента я буду писать код в OXXXml, потому что это единственный язык в что я могу доказать правильность кода ...

Может ли кто-то с большим опытом формальных инструментов доказательства прокомментировать? Опять же - я ЛЮБЛЮ использовать формальный инструмент проверки, я думаю, что они великолепны, но у меня сложилось впечатление, что они находятся в башне из слоновой кости, которую я не могу достать из скромного рва Java / C ++ ... (PS: я также ЛЮБЛЮ Haskell, OCaml ... не поймите неправильно: я фанат декларативных языков и формальных доказательств, я просто пытаюсь понять, как я могу реально сделать это полезным для разработки программного обеспечения)

Обновление: поскольку это довольно широкий вопрос, давайте попробуем ответить на следующие более конкретные вопросы: 1) есть ли примеры использования средств проверки, чтобы доказать правильность промышленных программ на Java / C ++? 2) Подойдет ли Coq для этой задачи? 3) Если подходит Coq, должен ли я сначала написать программу на Coq, а затем сгенерировать C ++ / Java из Coq? 4) Может ли этот подход обрабатывать потоки и оптимизацию производительности?

Фрэнк
источник
3
Я понимаю и оцениваю вашу проблему, но я не понимаю, что этот вопрос после (как сообщение SE). Обсуждение? Опыт? Ни один не подходит для SE. «Что я могу сделать?» Тон заставляет меня чувствовать, что это слишком широкий вопрос.
Рафаэль
3
Понятно ... согласен, этот вопрос не был четко сформулирован. Итак, скажем: 1) есть ли примеры использования пруверов для доказательства правильности промышленных программ на Java / C ++? 2) Подойдет ли Coq для этой задачи? 3) Если подходит Coq, должен ли я сначала написать программу на Coq, затем Coq сгенерирует C ++ / Java из этого? 4) Может ли этот подход справиться с поточностью и оптимизацией производительности?
Фрэнк
2
Итак, это четыре вопроса. 1) Вероятно, лучше в разработке программного обеспечения, так как вы вряд ли столкнетесь с (многими) отраслевыми специалистами здесь. 2) на вкус несколько субъективно, но у нас могут быть люди, которые могут предложить объективную перспективу. 3) насколько я могу судить, совершенно субъективно. 4) Хорошие вопросы для этого сайта. Подводя итоги: пожалуйста, разделите ваши вопросы, перейдите к разделу «Разработка программного обеспечения» первым и тщательно продумайте, можете ли вы ожидать объективного (!) Ответа здесь (!) Перед публикацией 2).
Рафаэль
10
Вы описываете мечту о формальной проверке, но мы очень далеки от этого. AFAIK, проверка программ не является обычной задачей и применяется только к очень простым программам. Тем не менее, я думаю, что этот вопрос актуален для сайта, и я был бы признателен за то, что кто-то из области признал пределы своей области, объясняя современное состояние и ограничения (возможно, путем ссылки на какой-то опрос ).
Юваль Фильмус
9
Проблема с проверкой программ на C ++ состоит в том, что C ++ не является четко определенным языком. Я не думаю, что широкомасштабная проверка возможна до тех пор, пока многие части программных систем (ОС, библиотеки, языки программирования) фактически не будут переработаны для поддержки проверки. Как хорошо известно, вы не можете просто сбросить 200 000 строк кода на кого-то и сказать «проверьте!». Вам нужно проверять и писать код вместе, и вам нужно адаптировать свои привычки программирования к тому, что вы также проверяете.
Андрей Бауэр

Ответы:

35

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

  1. Существует множество инструментов, специально разработанных для формального подтверждения свойств Java и C ++.

    Однако мне нужно сделать небольшое отступление: что значит доказать правильность программы? Средство проверки типов Java подтверждает формальное свойство Java-программы, а именно то, что некоторые ошибки, такие как добавление a floatи an int, никогда не могут возникнуть! Я предполагаю, что вы заинтересованы в гораздо более сильных свойствах, а именно в том, что ваша программа никогда не может войти в нежелательное состояние или что вывод определенной функции соответствует определенной математической спецификации. Короче говоря, существует широкий градиент того, что может означать «проверка правильности программы», от простых свойств безопасности до полного доказательства того, что программа соответствует детальной спецификации.

    Теперь я собираюсь предположить, что вы заинтересованы в доказательстве сильных свойств ваших программ. Если вас интересуют свойства безопасности (ваша программа не может достичь определенного состояния), то в целом, кажется, что лучший подход - это проверка модели . Однако, если вы хотите полностью указать поведение Java-программы, лучше всего использовать язык спецификации для этого языка, например, JML . Существуют такие языки для определения поведения программ на C, например, ACSL , но я не знаю о C ++.

  2. Когда у вас есть свои спецификации, вам нужно доказать, что программа соответствует этой спецификации.

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

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

    • Один инструмент, который анализирует код, спецификацию и генерирует теорему адекватности. Как упоминал Фрэнк, Кракатау является примером такого инструмента.

    • Один инструмент, который доказывает теорему (ы), автоматически или в интерактивном режиме. Таким образом Coq взаимодействует с Кракатау, и есть несколько мощных автоматизированных инструментов, таких как Z3, которые также можно использовать.

    Один (второстепенный) момент: есть некоторые теоремы, которые слишком трудно подтвердить с помощью автоматических методов, и известно, что автоматические средства проверки теорем иногда имеют ошибки в надежности, которые делают их менее надежными. Это область, где Coq сияет в сравнении (но это не автомат!).

  3. Если вы хотите сгенерировать код Ocaml, то сначала обязательно напишите в Coq (Gallina), а затем извлеките код. Однако Coq ужасен при создании C ++ или Java, если это вообще возможно.

  4. Могут ли вышеуказанные инструменты справиться с поточностью и проблемами производительности? Вероятно, нет, проблемы производительности и многопоточности лучше всего решаются специально разработанными инструментами, поскольку они представляют собой особенно сложные проблемы. Я не уверен, что у меня есть какие-либо инструменты, чтобы рекомендовать здесь, хотя проект Мартина Хофманна PolyNI кажется интересным.

В заключение: формальная проверка «реального мира» программ на Java и C ++ является большой и хорошо разработанной областью, и Coq подходит для выполнения части этой задачи. Вы можете найти общий обзор здесь, например.

Коди
источник
Спасибо за этот пост и за ссылки, которые вы добавили. ИМХО, цель для разработчиков программного обеспечения состоит в том, чтобы иметь возможность быстро выпускать системы, которые 1) всегда будут давать правильные результаты, 2) никогда не будут выходить из строя. Я мог видеть проблему регрессии здесь, где вы можете доказать, что сама спецификация «не содержит ошибок» :-) вроде как попытка определить «истинное предложение языка» с помощью метаязыка, а затем необходимость в другом мета-языке. язык для этого, затем еще один ...
Фрэнк
6
Проблема в том, что то, что «хочет» пользователь, обычно не выражается формальным языком! Обычно нет формального ответа на вопрос: «Соответствует ли эта формальная спецификация моей неформальной идее?». Можно протестировать формальную спецификацию и доказать, что она обладает определенными математическими свойствами, но в конечном итоге вам необходимо соотнести математику с реальным миром, который является неформальным процессом.
Коди
Да, конечно - я всегда понимал, что формальные методы могут начинаться только с четко определенной точки. Если эта спецификация соответствует или не соответствует осознанным / неосознанным / неоткрытым потребностям реальных пользователей, это еще одна проблема, не решаемая формальными методами (но, безусловно, проблема для инженеров).
Фрэнк
Теорема по определению является доказанным предложением. Таким образом, вы, вероятно, не имеете в виду «доказать теорему».
17
@nbro Википедия, похоже, согласна с вами. Mathworld, однако, определяет теорему как суждение, которое « может быть доказано как истинное с помощью принятых математических операций». В этом случае предоставление доказательств теорем не только возможно, но и необходимо оправдать, называя их так! :) (это, конечно,
противодействие
15

Я хотел бы упомянуть три замечательных применения формальных методов / инструментов формальной проверки в промышленности или нетривиальных реальных системах. Обратите внимание, что у меня мало опыта по этой теме, и я изучаю их только из чтения статей.

  1. Инструмент с открытым исходным кодом Java Pathfinder (сокращенно JPF), выпущенный НАСА в 2005 году, представляет собой систему для проверки исполняемых программ Java-байт-кода (см. Java Pathfinder @ wiki ). Он был использован для обнаружения несоответствий в исполнительном программном обеспечении для K9 Rover в НАСА Эймс.

  2. Эта статья: Использование проверки моделей для поиска серьезных ошибок файловой системы @ OSDI'04 показывает, как использовать проверку моделей для поиска серьезных ошибок в файловых системах. Система под названием FiSC применяется к трем широко используемым, тщательно протестированным файловым системам: ext3, JFS и ReiserFS, и обнаружено 32 серьезных ошибки. Он выиграл награду за лучшую бумагу.

  3. В этом документе: Как веб-службы Amazon используют формальные методы @ CACM'15 описывает, как AWS применяет формальные методы к своим продуктам, таким как S3, DynamoDB, EBS и диспетчер внутренней распределенной блокировки. Основное внимание уделяется инструменту Lamport TLA + . Кстати, Лампорт интенсивно использовал свой собственный набор инструментов TLA. Он часто дает (довольно полную) формальную проверку в TLA алгоритмов / теорем, предложенных им (а также соавторами) в приложениях к статьям.

Hengxin
источник
4

Формальная спецификация программы - это (более или менее) программа, написанная на другом языке программирования. В результате, спецификация, безусловно, будет содержать свои ошибки.

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

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

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

vonbrand
источник
Преимущество формальной проверки является то , что .... Вторым недостатком формальной проверки является то , что ... Это сбивает с толком.
hengxin
Я думаю, что несоответствие между спецификацией и неформальной задачей является проблемой анализа требований к программному обеспечению, а не проблемой программирования.
Каве
3

Формальная проверка теперь возможна для программ, написанных подмножеством C ++, предназначенных для критичных для безопасности встроенных систем. См. Http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.ppt для краткой презентации и http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf для полной статьи.

dc42
источник
5
Спасибо за ссылки. По крайней мере, краткий обзор их содержания был бы полезен для защиты от гниения ссылок, тем более что ваши ссылки ведут на корпоративный веб-сайт: они, как правило, периодически реорганизуются, убивая все ссылки на сайт.
Дэвид Ричерби
2

Вы задаете несколько разных вопросов. Я согласен, что кажется, что формальные методы проверки для промышленных / коммерческих приложений не так распространены однако следует понимать, что многие принципы «формальной проверки» встроены в компиляторы для определения правильности программы! таким образом, если вы используете современный компилятор, вы используете большую часть современного уровня в формальной проверке.

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

Вы упоминаете Java. Есть много продвинутых формальных методов проверки, встроенных в программу проверки Java под названием FindBugs, которые действительно могут работать на больших кодовых базах. Обратите внимание, что в результате появятся как «ложные срабатывания, так и ложные отрицания», и результаты должны быть рассмотрены / проанализированы разработчиком-человеком. Но обратите внимание, что даже если он не выявляет реальных функциональных дефектов, он обычно выявляет «антипаттерны», которых в любом случае следует избегать в коде.

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

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

Вот пример исследования формальных инструментов проверки в области ЭЭ, проведенного Ларсом Филипсоном .

ВЗН
источник
2
Вводить в заблуждение утверждение о том, что «многие принципы« формальной проверки »встроены в компиляторы для определения правильности программы». Вы ссылаетесь на статическую проверку типов, которую делают некоторые компиляторы, но свойства, проверенные таким образом, довольно просты, например, избегают добавления числа и строки. Это полезно, но далеко от того, что обычно понимается под «формальной проверкой».
Мартин Бергер
2
конкретно не упоминается о статической проверке типов, хотя это один простой / общий пример. Методы оптимизации компилятора imho, которые широко распространены и продвинуты, примерно аналогичны формальным принципам проверки, потому что они включают в себя передовые методы для определения / отображения эквивалентности оптимизированных вариантов программы. так что, похоже, здесь важно избегать проблемы «движущихся ворот» и не предполагать, что только потому, что компилятор делает это или встроен в компилятор, это не формальная проверка.
ВЗН
2
согласился, что это не общее понимание. грубо говоря, методы оптимизации создают модель поведения программы, например, цикла или подпрограммы, и оптимизируют эту модель, а затем генерируют новый код, который доказуемо эквивалентен. поэтому некоторые из этих оптимизаций довольно сложны в перестановке кода, и для меня они используют формальные принципы проверки. похоже, в компиляторе есть много других примеров формальных методов проверки ... первоначальный вопрос задавал много разных вопросов, как отмечали многие, я не пытаюсь ответить на все содержащиеся в нем вопросы.
13
2
кстати, в JRE, java runtime engine, например, динамическая оптимизация и т. д., также используются некоторые формальные принципы верификации
vzn
3
это « мечта о формальной проверке», о которой упоминал фильм, выше, имхо, химерная абстракция, и прагматичная / утилитарная / реалистичная индустрия в значительной степени признает ее как таковую. в течение десятилетий известно, что большие кодовые базы по своей природе имеют ошибок / дефектов на K-строк кода, и это никогда не изменится, независимо от того, как продвигается теория / технология, это факт человеческой природы. и на самом деле созданные человеком математические теоремы обладают такими же свойствами, хотя это широко не ценится! уxy
2011 года
1

Возможно, модель проверки может быть полезной.

http://alloytools.org/documentation.html Alloy - это средство проверки моделей.

Хорошая презентация, объясняющая концепцию проверки модели с использованием Alloy: https://www.youtube.com/watch?v=FvNRlE4E9QQ

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

ТИК Так
источник