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