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

Question

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

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

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

Answer 1

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

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

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

Не удовлетворенный assert() и взволнованный проектом Design by Contract, я решил создать свою собственную реализацию Design by Contract для C. Посмотрев некоторые решения, доступные для Java 1, я решил использовать подмножество языка Object Constraint Language для экспресс-контракты [4]. Используя Ruby и Racc, я создал Design by Contract для C, генератор кода, который превращает контракты, встроенные в комментарии C, в код C для проверки контрактов.

Answer 2

Open-Source: проверить.

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

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

Answer 3

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

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

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