Проектирование по контракту в C для использования в автоматическом доказательстве теорем

Question

Я работаю над парой проектов на C и хотел бы использовать автоматическое доказательство теорем для проверки кода. В идеале я просто хотел бы использовать ATP для проверки контрактов функций. Есть ли какая-либо функциональность в C / gcc или внешнем программном обеспечении / пакетах / и т. Д., Которая позволила бы кодировать стиль по контракту?

Если нет, то это просто стимул начать самостоятельно.

Мои ссылки на это будут что-то вроде Spec # или Sing # из MSR, но я парень с открытым исходным кодом и ищу решения с открытым исходным кодом.

Answer 1

Open-Source: проверка

.

Автоматическое доказательство теорем: проверка.

Вам действительно понравится Frama-C и язык спецификации ACSL Возможно, вы уже слышали о его предке Caduceus, но в настоящее время он считается замененным Frama-C / Jessie.

Answer 2

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

Тот, что в RubyForge, Дизайн по контракту для C , выглядит очень многообещающе. GNU Nana существует уже давно и, вероятно, удовлетворит ваши потребности. Надеюсь, что это полезно.

Редактировать: Проверить эту статью в O'Reily на дизайн по контракту для C:

Не устраивает assert () и взволнован дизайн по контракту, я намеревался создать свой собственный дизайн Выполнение контракта на C. После глядя на некоторые решения доступно для Java 1 Я решил использовать подмножество ограничений объекта Язык для выражения контрактов [4]. Используя Ruby и Racc, я создал дизайн по контракту для C, генератор кода что превращает контракты, встроенные в C комментарии в коде C, чтобы проверить контракты.

Answer 3

Если вы заинтересованы в проверке кода C с использованием средств доказательства теорем, вам следует проверить проект VCC . С их веб-страницы:

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

VCC - очень зрелая система из Microsoft Research , и она использовалась для проверки гипервизора Microsoft Hyper-V . VCC также с открытым исходным кодом.