проверка — есть ли способ доказать свойства моих программ на C ++?
Я понимаю, как такие языки, как Coq и Idris, можно использовать для доказательства свойств программ, написанных на этих языках (судя по моему небольшому опыту в этой области), но мне интересно, есть ли приемлемый способ сделать то же самое внешне, на уже существующей кодовая.
Есть ли способ использовать такой инструмент, как Coq, или какой-либо другой специализированный инструмент, чтобы доказать правильность алгоритмов, написанных на C ++? Если да, каковы требования для этого?
Решение
Это зависит от того, что вы подразумеваете под «доказательством собственности». Насколько я знаю, существует множество инструментов статического анализа для проверки простых свойств программ на Си, и они сильно различаются в плане выразительности, простоты использования, надежности анализа и т. Д. Они обычно используются для проверки того, что программы бесплатны. ошибок во время выполнения, но они не очень хороши для проверки полных функциональных спецификаций. Для этого типа свойств вам, возможно, придется прибегнуть к более мощному испытателю, который требует, чтобы вы вручную записали доказательство, а не проверяли его автоматически.
Поскольку вы упоминаете Coq, я хотел бы отослать вас к двум инструментам на основе Coq для проверки программ на C (однако они не работают с C ++): в последней категории есть Проверенный программный инструментарий, логика рассуждений о программах на C, встроенная в Coq. Вы можете использовать его для написания доказательств о поведении вашей программы и заставить Coq проверить их, в том числе показать, что программа соответствует своей функциональной спецификации. По первой категории есть Verasco, инструмент автоматического статического анализа, который проверяет вашу программу на отсутствие ошибок во время выполнения. Одной из приятных особенностей этих инструментов является то, что они сами являются проверенными программами, а это означает, что вы можете иметь дополнительную степень уверенности в проводимых ими анализах.
Другие интересные инструменты включают Frama-С, как упоминалось в комментарии выше, и VCC, статический анализатор от Microsoft. Однако они не работают с C ++.
Другие решения