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.
Asked By : fossdeep
Answered By : babou
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.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/43738
0 comments:
Post a Comment
Let us know your responses and feedback