Menu
First of all, is this only possible on algorithms which have no side effects?
Secondly, where could I learn about this process, any good books, articles, etc?
352
The only way to prove the correctness of an algorithm over all possible inputs is by reasoning formally or mathematically about it. One form of reasoning is a "proof by induction", a technique that's also used by mathematicians to prove properties of numerical sequences.
A verification algorithm is a two-argument algorithm A, where one argument is an ordinary input string x, and the other argument is a binary string y called a certificate. Algorithm A verifies x if there exists a y such that A(x,y) = 1.
A proof of correctness is a mathematical proof that a computer program or a part thereof will, when executed, yield correct results, i.e. results fulfilling specific requirements. Before proving a program correct, the theorem to be proved must, of course, be formulated.
correctness and efficiency, where correctness means that a right result is obtained for all possible problem instances (size of the data structure, state of the input — sorted, unsorted, random, nearly-sorted etc), while efficiency means how the time and computer resources needed to successfully carry out the algorithm ...
COQ is a proof assistant that produces correct ocaml output. It's pretty complicated though. I never got around to looking at it, but my coworker started and then stopped using it after two months. It was mostly because he wanted to get things done quicker, but if you need to verify an algorithm this might be a good idea.
Here is a course that uses COQ and talks about proving algorithms.
And here is a tutorial about writing academic papers in COQ.
145
39
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
