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.