Quality Assurance II -------------------------------------- slide number 1 Quality Assurance II ______________________________ Outline These slides will be covered during TWO lectures. Introduction Formal Verification Theoretical Limits Quality Assurance II -------------------------------------- slide number 2 Software Quality Previous discussions relating to QA have focused on * process quality * related to the currently popular Demming notions * manifested in QA plans * testing * most important technical part of QA * testing has two levels - strategy and tactics * metrics * error tracking & prediction Quality Assurance II -------------------------------------- slide number 3 Software Quality Assurance Process * methods and tools * configuration management and change control * standards and standard compliance mechanisms * reporting mechanisms Verification and Validation * formal technical reviews * multi-tiered testing strategy * measurement o symbolic execution => formal verification techniques Quality Assurance II -------------------------------------- slide number 4 Verification versus Validation Verification: "Are we building the product right?" * implementation meets specifications Validation: "Are we building the right product?" * specifications meet needs Quality Assurance II -------------------------------------- slide number 5 Symbolic Execution Goal: reason about history of value changes Represent * values with character strings * operations by augmented strings == trace For example: readf "%d", x; y := x + 2; z := y + 3; sets x <= "input" y <= "input + 2" z <= "(input + 2) + 3" * expression simplification Quality Assurance II -------------------------------------- slide number 6 Formal Verification Program Proving * vitally dependent on specification formal verification can only be done against a formal specification Techniques * assertions * formal semantics In depth * P415/P515 Introduction to Verification Quality Assurance II -------------------------------------- slide number 7 Basic Idea Each statement S is surrounded by logical formulae F1 and F2 Notation: { F1 } S { F2 } Interpretation: In a -c-o-r-r-e-c-t--p-r-o-g-r-a-m-, if F1 is true before S, then F2 is true afterwards. F1 is called a pre-condition for S F2 is called a post-condition for S Both are called assertions Quality Assurance II -------------------------------------- slide number 8 Assertions * for example {y>5} x := y-2 {x>3 & y>5} * in a program: - always possible as comments - some languages provide ASSERT statements ASSERT y > 5; x := y - 2; ASSERT x > 3 & y > 5; * can "chain" assertions { F1 } S1 { F2 } S2 { F3 } Quality Assurance II -------------------------------------- slide number 9 Formal Deduction Program with assertions are manipulated in a formal deduction system based on proof rules, such as {F1} S1 {F2} , {F2} S2 {F3} __________________________ {F1} S1 ; S2 {F3} These proof rules are in the same spirit as the proof rules of "classical" logic, such as A , A => B ___________ B Quality Assurance II ------------------------------------- slide number 10 Assertions and Loops Loop Invariant: an assertion preserved by the -b-o-d-y-of a loop If {F} is invariant for a particular loop (body) then {F} is preserved by the entire loop proof: by induction on number of iterations Write {{F}} to indicate F is a loop invariant Quality Assurance II ------------------------------------- slide number 11 Example Procedure Procedure BubbleSort( A: ARRAY OF INT, lim: INT ); for i := 2 to lim do j := i; while j>1 and A[j]1 and A[j]1 and A[j]1 and A[j] y } {{ x > y }} while x <> 0 do x := x-2 ; y := y-2 ; end { x > y & x = 0 } The proof rule shows the above to be correct but the loop terminates if and only if x is initially even and positive. Quality Assurance II ------------------------------------- slide number 17 Loop Invariants and Induction Tail recursion => iteration f( i, x ) := if ( i=0 ) then g(x) else h( i, f( i-1, x ) ) becomes f( m, x ) { r := g(x); for i = m until 1 do r := h( i, r ); return r } Loop invariant on iterative version is very close to induction on recursive version Quality Assurance II ------------------------------------- slide number 18 Loop Invariants as Design Aid Formalism is -n-o-t-necessary Ask: * What is changed in this loop? * What is preserved in this loop? Look for higher-level concepts/properties (such as part of array being sorted) Quality Assurance II ------------------------------------- slide number 19 Back to Termination It would be valuable to have a method to discover whether or not a program terminates. Why not just run it? * Fundamental limitation to computer science Quality Assurance II ------------------------------------- slide number 20 The Halting Problem (A problem is a set of inputs which we would like to classify by some program.) Q: Can we tell whether or not an arbitrary program halts? A: In general, no! Intuition for the proof: This statement is false. true => false false => true This contradiction requires: +o self-reference +o negation Quality Assurance II ------------------------------------- slide number 21 Statement & Proof Outline Theorem: It is impossible to write a procedure that decides whether an arbitrary program halts. Outline: proof by contradiction 1. assume the result is false (i.e. such a procedure -d-o-e-s-exist) 2. define a new program using assumption 3. consider cases when this new program halts a. if it halts => it doesn't b. if it doesn't => it does hence program cannot be constructed, so procedure does not exist. Quality Assurance II ------------------------------------- slide number 22 Proof - Step 1 Assume there is a Boolean procedure DoesHalt? such that: DoesHalt?(Pfile) returns -t-r-u-e-if the program represented by Pfile halts and -f-a-l-s-e-if the program goes into an infinite loop. Preconditions: a. Pfile is a text file b. Pfile represents a syntactically correct program Postconditions: a. Pfile is not changed b. The value -t-r-u-e-or -f-a-l-s-e-is returned as indicated above Quality Assurance II ------------------------------------- slide number 23 Proof - Step 2 On the file Confound put the program: /* file Confound */ main( ) #include DoesHalt? { if (DoesHalt?( __________ )) { /* loop forever */ while ( true ) { }; } } (will fill in "__________" later) That is, the program Confound halts if DoesHalt?(__________) is FALSE but it loops forever if DoesHalt?(__________) is TRUE. Quality Assurance II ------------------------------------- slide number 24 A "Thought Experiment" Pretend to execute the program by: 1. compiling the program file Confound 2. running the compiled program That is: %cc Confound %a.out What would happen??? Would it halt??? Quality Assurance II ------------------------------------- slide number 25 Proof - Step 3 Two cases: DoesHalt? in Confound o either returns -T-R-U-E- o or it returns -F-A-L-S-E-: case 1 - DoesHalt?("Confound") is TRUE => the program loops => DoesHalt?("Confound") is FALSE case 2 - DoesHalt?("Confound") is FALSE => the program halts => DoesHalt?("Confound") is TRUE Quality Assurance II ------------------------------------- slide number 26 Consequences of Halting Problem * halting problem takes on many "disguises" * virtually any program that takes other programs as input is vulnerable: * compiler optimization dead code eliminantiIoFn's, 2n possible paths * program verification * concurrency synchronization * expert systems * sometimes restrict power to avoid trap * SQL, other database query languages exhaustive testing impossible * in general, a valuable warning Proving that many conditions are mutually exclusive => many fewer possible paths Q=u>alityeAxshsauursatnicvee ItIes-t-s--m-a-y--b-e--p-o-s-s-i-b-l-e------------------- slide number 27 Testing and Formal Verification Recall the complexity problem with testing a long chain of IF's: Quality Assurance II ---------O-M-I-T-T-E-D--f-i-g-u-r-e--------------- slide number 28 Proofs in Practice * dependence on formal specifications => cannot prove systems with complex interactions * program proving useful for critical internal modules - abstract data types (ADT's) - synchronizations * proofs complement testing useful for hard-to-test situations Quality Assurance II ------------------------------------- slide number 29 Proofs in Practice Just as the typical mathematician does not prove theorems using the predicate calculus, the typical computer scientist should not prove programs by formal deduction. Hence * human-readable proofs * "programmer's assistant" to handle details * CASE tools should facilitate use of assertions Proof-like algorithms often internal * type checking * database validation Quality Assurance II ------------------------------------- slide number 30 Example: Trusted Agents Goal: admit "foreign" code inside of "firewall" Application: network protocol checkers small, quick Traditional approaches: interpretation, bounds checking essentially, a mini-firewall Alternative: foreign module -i-n-c-l-u-d-e-s-both code & -p-r-o-o-f-of proper behavior * use the fact that proof -c-h-e-c-k-i-n-g-is easy even if proof -d-i-s-c-o-v-e-r-y-is hard Quality Assurance II ------------------------------------- slide number 31 Ten Commandments of Formal Methods 1. choose appropriate notation 2. formalize but don't over-formalize 3. estimate costs 4. have a formal methods expert on call 5. augment rather than replace traditional methods 6. document sufficiently 7. don't compromise other quality standards 8. do not be dogmatic 9. test, test, and test again 10. reuse - after Bowan and Hinchley, Computer April 1995 Additional Reading: R. A. DeMillo, R. J. Lipton, & A. J. Perlis, "Social Processes and Proofs of Theorems and Programs," Comm. ACM 22,5 (May 1979), 271-280. responses Comm. ACM 22,11 (Nov. 1979) 621-630. D. L. Parnas, "Software Aspects of Strategic Defense Systems," Comm. ACM 28,12 (Dec. 1985), 1326-1335. responses Comm. ACM 29,7 (July 1986), 591-592; 29,9 (Sept 1986), 830-831. Copyright 2109-2-16, Edward L. Robertson