Есть ли способ доказать свойства моих программ на C++?

Question

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

Есть ли способ использовать такой инструмент, как Coq, или какой-либо другой специализированный инструмент, чтобы доказать правильность алгоритмов, написанных на C++? Если да, то каковы требования для этого?

Answer 1

Это зависит от того, что вы подразумеваете под «доказательством собственности». Насколько мне известно, существует множество инструментов статического анализа для проверки простых свойств программ на C, и они широко варьируются с точки зрения выразительности, простоты использования, обоснованности анализа и т. Д. Они обычно используются для проверки того, что программы бесплатны ошибок во время выполнения, но не очень хороши для проверки полных функциональных спецификаций. Для такого рода свойств вам, возможно, придется прибегнуть к более мощным средствам проверки, которые требуют, чтобы вы вручную записали доказательство, вместо того, чтобы один из них проверял вас автоматически.

Поскольку вы упомянули Coq, я хотел бы направить вас к двум инструментам Coq для проверки программ на C (они не работают с C++, однако): в последней категории есть Verified Software Toolchain, логика для рассуждения о программах C, встроенных в Coq. Вы можете использовать его для написания доказательств поведения вашей программы и проверить их Coq, в том числе показать, что программа соответствует его функциональной спецификации. В первой категории есть Verasco, инструмент автоматического статического анализа, который проверяет вашу программу на отсутствие ошибок во время выполнения. Одна из приятных особенностей этих инструментов заключается в том, что они сами являются проверенными программами, подразумевая, что вы можете получить дополнительную уверенность в анализе, который они предоставляют.

Другие интересные инструменты включают в себя Frama-C, как упоминалось выше, и VCC, статический анализатор от Microsoft. Однако они не работают с C++.