6
$\begingroup$

Does anyone have any complete example of a proof of program correctness? I'm talking about something that includes the usual predicate, base case, inductive hypothesis, and inductive step. But also important is the loop invariant, and termination. I'm just not sure what the proper format for something like this is.

The only things I've been able to find are powerpoint slides from random schools, but they are for teaching purposes, and all over the place. I'm looking for something from start to finish, easy to follow, and formatted nicely that it can be submitted academically.

I wish to understand what a program proof looks like when (if) it is used for real, rather than as a proof sketch for a toy example in the classroom.

$\endgroup$
  • 3
    $\begingroup$ There are loooots of them in CLRS. What exactly are you looking for? $\endgroup$ – hengxin Jun 19 '15 at 3:06
  • 1
    $\begingroup$ Something online and free? :) $\endgroup$ – fossdeep Jun 19 '15 at 4:19
  • 2
    $\begingroup$ You want to submit something academically, ask other people to do it for you, and don't want to visit a library? Huh. $\endgroup$ – Raphael Jun 19 '15 at 11:14
  • $\begingroup$ I don't want anyone to do it for me. $\endgroup$ – fossdeep Jun 19 '15 at 14:01
  • $\begingroup$ There are multiple free, online algorithms textbooks. Take a look at them to see if any of them meet your eneds. $\endgroup$ – D.W. Jun 19 '15 at 17:20
7
$\begingroup$

You will find a collection of proof techniques illustrated with poofs of small programs in the following paper:

Inductive Methods for Proving Properties of Programs, Manna, Ness, Vuillemin, CACM 16-8, August 1973.

It is made available on the web by one of the authors. It is also the first paper I ever read on the subject, and I remember enjoying it.

But I would expect the literature, on and off the web, refereed papers, textbooks and other sources. to include a considerable number of such proofs, considering that today people are working on the proofs of real program (such as compilers), with the help of mechanized proof systems.

OF course, you are aware that there is no such thing as correctness in an absolute sense. Correctness is defined only with respect to some specification, i.e. to some predicate in a logic that can also express the meaning of programs (or whatever part of it is relevant).

Of course, there are different ways of defining the semantics of a program. So one might expect to have proof techniques that vary accordingly.

$\endgroup$
  • $\begingroup$ I do have a textbook that explains these things. It's similar to the one you showed, but both don't have an example proof from start to finish without random notes everywhere. I guess it's like you say, there is nothing formal. Also, I've been told that the people who write these proofs are programmers. So I'm going to assume they show it to their bosses, then scrap it after the program has been written. $\endgroup$ – fossdeep Jun 19 '15 at 19:53
  • 2
    $\begingroup$ @fossdeep Actually, proving (properties of) programs in real life is quite difficult, and probably beyond the competence of most programmers. It is also nothing that their boss wants to read. People who make these proofs are either algorithm designers (you do not publish an algorithm without some kind of proof), or proof specialist for complex programs. Both are mathematicians. For actual programs, proofs are conducted on proof assistant systems, which do most of the error checking. It is more a matter of process, than a final document with a written proof on it. Only the computer sees that. $\endgroup$ – babou Jun 19 '15 at 20:20
  • 1
    $\begingroup$ @fossdeep In other words, it is exactly the opposite of scraps of paper. For algorithms you ave formal academic papers. For complex programs you may have proof assistants, very systematic and using no paper at all. I am not saying that proof assistant are not used for algorithms. This is only to give you a quick sketch of situations that can be encountered. It is real science ... you want proofs to give you assurance, hence you want a process that can be trusted. $\endgroup$ – babou Jun 19 '15 at 20:27
  • $\begingroup$ Interesting. Didn't know that. Thanks. $\endgroup$ – fossdeep Jun 19 '15 at 22:14
  • $\begingroup$ @fossdeep Among the major motivations in industry, you have safety of life critical devices (vehicles, or medical equipment for example), and also reliability of cryptographic system. They also do a lot of program proving in space industry because silly bugs just cost to much money. So the cost of proving correctness is worth paying. $\endgroup$ – babou Jun 19 '15 at 22:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.