15. Formal ProofsHoare TriplesAssignment RuleRule of ConsequenceComposition RuleIF-THEN-ELSE RuleReal-World ExampleAbsolute Value ExampleIF-THEN RuleWHILE RulePostcondition Obligation: Let us see if it can be used to prove the postcondition of the Program Hoare Triple (Postcondition Obligation):Precondition Obligation: We also need to show that the invariant is true the first time the loop is encountered in this program (Precondition Obligation):Invariant Obligation: We have one last step left, which is to prove that:Partial CorrectnessWhy FormalUnderstanding a Programming Language: We have seen that it is possible to formally define the semantics of programming language constructs rather than relying on English. For instance, the assignment rule succinctly explains the meaning of assignment. These formal semantics help us understand more deeply the nature of programs.Finding Boundary Conditions: Proofs help us find boundary conditions. For instance, my first attempt at the asserted summation program was:Complex Compact Code: It is possible that some of these errors can be discovered more quickly during debugging. However, proofs are superior to debugging when you write some complex compact code, which cannot be so easily debugged. They do not work very well with large complex code such as our spreadsheet, since the proofs can become harder to understand than the programs themselves. So the moral is to use them for portions of the program that are tricky rather than the whole program.COMP 114, Spring 1998Prasun Dewan115. Formal ProofsHow do we know that the assertions we make about a program are valid, that is, describe the actual behavior of the program ? In fact, the discussion so far assumed we did not know, and in debugging we findout about the validity of our assertions. But debugging can only test a finite number of cases. So if our assertions do not fail in the test cases we try, that does not mean they are valid. (When an assertion is invalid, either the program is wrong, that is, it is not meeting the specification; or the assertion is wrong, that is, it is not an accurate description of the program.)There is a whole body of literature on formally proving the validity of assertions. It depends on there being a formal definition of each language construct we use in our program, and using these definitions to prove our assertions about a program.Hoare TriplesThis work was pioneered by Hoare, who invented the idea of precondition and postcondition of a statement. In fact, the triple:(precondition, statement, postcondition) is called a Hoare triple. We will use a different syntax from the one we have used so far to write this triple:[precondition]statement[postcondition]The following example shows the syntax:[true]x = 3[x == 3]This is more or less the traditional method for writing Hoare triples. The difference is that the traditional method uses { instead of [:{true}x = 3{x == 3}We have made the substitution because Java uses { for statement blocks and we need to distinguish betweenassertions and statements. The advantage of this syntax over the one we used:pre: truepost: x == 3x = 31  Copyright Prasun Dewan, 1998.1is that it easily allows the postcondition of a statement to become the precondition of the next statement, which is useful in proving assertions about a sequence of statements.Assignment RuleLet us look again at the example:[true]x = 3[x == 3]How do we know this is a valid Hoare triple? We know from our informal understanding of assignment thatthis is the case. Here is a formal description of assignment that can be used to derive this triple:[Q(v /e)] v = e [Q] – Assignment RuleIt says that the triple of the form above is valid. The term: Q(v /e) is a proposition constructed from Q by replace all occurrences of v with e. Thus, if Q is:x == 3Q (v/e) is:3 == 3So from this rule, we can derive that the following triple is valid:[3 == 3]x = 3[x == 3]or[true]x = 3[x == 3]is valid, which is what we wanted to prove.What if we wanted to prove:[y == 3]x = 3[y == 3]is valid? If we replace all (zero) occurrences of x in y == 3, we get y == 3, so the rule straightforwardly implies this triple. Rule of ConsequenceWhat we have seen above is one rule for generating valid Hoare triples. Let us look at a few other rules. Before we do this, we need a convenient notation to indicate implication or inference. If p => q we will sometimes write it as:2p_qMoreover we will sometimes omit the & operation between propositions. Thus:p q__rsays p & q => rWe can now give two additional rules: [P] S [Q] Q => Q’_____________________ ---- Rule of weakened postcondition [P] S [Q’]P’ => P [P] S [Q] _____________________ ---- Rule of strengthened precondition [P’] S [Q]We actually have already seen these before, when justifying weakest precondition and strongest postconditions. They say: if [P] S [Q] is a valid Hoare triple, and Q => Q’, then [P] S [Q’] is a valid Hoare triple, since once we have established Q, we can establish the weaker postcondition, Q’.  if [P] S [Q] is a valid Hoare triple, and P’ => P, then [P’] S [Q] is a valid Hoare triple, since if we can establish P’, we can meet the weaker precondition, P, of S.We can combine these rules as follows:P’ => P [P] S [Q] Q => Q’_____________________ ---- Rule of consequence [P’] S [Q’]Composition RuleAnother rule has to do with the composition of statements:S1;S2In general, the precondition of the composition of statements, S1;S2, is at least as strong as the preconditionof S1 since the constraints of both statements must be met. If the postcondition of S1 is the precondition of S2, then the precondition of S1 is also the precondition of S1;S2, since after executing S1, we have established the precondition of S2. The postcondition of S1;S2 becomes the postcondition of S2:[P] S1 [Q] [Q] S2 [R]_________________ -------- Composition Rule[P] S1; S2 [R]IF-THEN-ELSE Rule3Consider the if-then-else statement:if B S1else S2If we know the pre and post conditions of S1 and S2, what can we say about the pre and post conditions of the if-then-else statement?Real-World Example To help understand the if-then-else semantics, let us take a real-world analogy. Consider the two introductory CS courses: Comp 14 and Comp 15. The Hoare triple for Comp 15 is:[Some Previous Programming Experience] & [High School Math] Comp 15[Significant Programming