CSE115/ENGR160 Discrete Mathematics 04/12/114.5 Program correctnessProgram verificationSlide 4Partially correctHoare tripleRules of inferenceSlide 8Conditional statementsSlide 10Condition statementSlide 12Slide 13Slide 14Slide 15Loop invariantsSlide 17ExampleSlide 19Slide 20Slide 21Slide 22Slide 23CSE115/ENGR160 Discrete Mathematics04/12/11Ming-Hsuan YangUC Merced14.5 Program correctness•Suppose we have designed an algorithm to solve a problem with a program•After debugging, how can we be sure that the program always get the correct answer?•Need a proof to show that the program always gives the correct answer•Program verification: uses the rules of inference and proof techniques2Program verification•One form of formal verification•It can be carried out using a computer•However, only limited progress has been made•Some mathematicians and theoretical computer scientists argue that it will never be realistic to mechanize the proof of correctness of complex programs3Program verification•A program is said to be correct if it produces the correct output for every possible input•A proof that a program is correct consists of two parts–Partial correctness: Correct answer is obtained if the program terminates–Shows the program always terminates4Partially correct•To specify a program produces the correct output–Initial assertion: the properties that the input values must have–Final assertion: the properties that output of the program should have, if the program did what was intended•A program or program segment, S is said to be partially correct with respect to the initial assertion p and the final assertion q if whenever p is true for the input values of S and S terminates, then q is true for the output values of S. •The notation p{S}q indicates that the program, or program segment, S is partially correct with respect to the initial assertion p and the final assertion q5Hoare triple•The notation p{S}q is known as one Hoare triple•Show that the program segment y:=2 z:=x+y is correct w.r.t. the initial assertion p: x=1 and the final assertion q: z=3•Suppose that p is true, so that x=1. Then y is assigned the value 2, and z is assigned the sum of the values of x and y, which is 3.•Hence, S is correct w.r.t the initial assertion p and the final assertion q. Thus p{S}q is true6Rules of inference•Suppose the program S is split into subprograms S1 and S2, denote it by S=S1;S2 •Suppose the correctness of S1 w.r.t. the initial assertion p and final assertion q, the correctness of S2 w.r.t. the initial assertion q and the final assertion r•It follows if p is true and S1 is executed and terminates, then q is true; and if q is true and S2 executes and terminates, then r is true7Rules of inference•This, if p is true and S=S1;S2 is executed and terminates, then r is true•This rule of inference, called the composition rule can be stated as 8rSSprSqqSp};{}{}{2121Conditional statements•Consider a program statement if condition then S•To verify this segment is correct w.r.t. initial p and final assertion q, two things must be done–First, when p is true and condition is true, then q is true after S terminates–Second, when p is true and condition is false, then q is true (as S is not executed)9Conditional statements•The rule of inference 10qSconditionpqconditionpqSconditionp} then if{)(}){(Condition statement•Verify the program segment if x > y then y:=x is correct w.r.t the initial assertion T and the final assertion y≥x•When the initial assertion is true and x>y, then the assignment y:=x is carrier out. Thus, the final assertion is true•When the initial assertion is true and x>y is false, so x≤y, and the final assertion is true•Hence, using the rule of inference for conditional statements, this program is correct w.r.t. the given initial and final assertions11Conditional statements•if condition then S1 else S2•To verify this program segment is correct w.r.t. the initial assertion p and the final assertions q•First, show that when p is true and condition is true, then q is true after S1 terminates•Second, show that when p is true and condition is false, then q is true after S2 terminates12Conditional statements•The rule of inference13qSSconditionpqSconditionpqScondi tionp} else then if{}){(}){(2121Conditional statements•Verify the program segment if x < 0 then abs:=-x else abs:=x is correct w.r.t. the initial assertion T and the final assertion abs=|x|•Two things must be demonstrated. First, it must be shown that if the initial condition is true and x<0, then abs=|x|. This is correct as when x<0, the assignment statement abs:=-x sets abs=-x, which is |x| by definition when x<014Conditional statements•Second, it must be shown that if the initial assertion is true and x<0 is false, so that x≥0, then abs=|x|. This is correct as in this case the program uses the assignment abs:=x, and x is |x| by definition when x≥0, so that abs:=x•Hence, using the rule of inference for program segments of this type, this segment is correct w.r.t. the given initial and final assertions15Loop invariants•Proof of correctness of while loops while condition S•Note that S is repeatedly executed until condition becomes false•An assertion that remains true each time S is executed must be chosen•Such an assertion is called a loop invariant•That is, p is a loop invariant if (p∧condition){S}p is true16Loop invariants•Suppose that p is a loop invariant, it follows that is p is true before the program segment is executed, p and ¬condition are true after terminates, if it occurs 17)}( while{}){(pconditionSconditionppSc onditionpExample•A loop invariant is needed to verify the segment i:=1 factorial:=1 while i<n begin i:=i+1 factorial:=factorial∙i end terminates with factorial=n! when n is a positive integer18Example•Let p be the assertion “factorial=i! and i≤n”. We first prove that p is a loop invariant•Suppose that at the beginning of one execution of the while loop, p is true and the condition holds, i.e., assume that factorial=i! that i<n•The new values inew and factorialnew of i and factorial are inew=i+1≤n and factorialnew=factorial ∙(i+1) = (i+1)! = inew!•Because i<n, we also have inew=i+1≤n•Thus p is true at the end of the execution of the loop•This