I understand how languages like Coq and Idris can be used to prove properties of programs written in those languages (judging by my little experience in the subject.), but I wonder if there's an approachable way to do the same externally, on an already existing codebase.
Is there a way to use a tool like Coq, or some other specialized tool, to prove correctness on algorithms written in C++? If so, what are the requirements for doing so?
It depends on what you mean by "proving a property". As far as I know, there are many static analysis tools for checking simple properties of C programs, and they vary widely in terms of expressiveness, ease to use, soundness of the analysis, etc. They are typically used for checking that programs are free of run-time errors, but aren't very good for checking complete functional specifications. For this kind of properties, you might have to resort to a more powerful prover that requires you manually write down a proof, instead of having one checked for you automatically.
Since you mention Coq, I would like to refer you to two Coq-based tools for verifying C programs (they don't work with C++, however): on the latter category, there is the Verified Software Toolchain, a logic for reasoning about C programs that is embedded inside Coq. You can use it for writing proofs about your program's behavior and have Coq check them, including showing that a program meets its functional specification. On the former category, there is Verasco, an automatic static-analysis tools that inspects your program for the absence of run-time errors. One nice feature of these tools is that they are themselves verified programs, implying that you can have an additional degree of confidence in the analyses they deliver.
Other interesting tools include Frama-C, as mentioned in the comment above, and VCC, a static analyser from Microsoft. They don't work with C++, however.
© 2022 - 2024 — McMap. All rights reserved.
