Kĩ thuật lập trình - Chapter 18: Program correctness

Programming Languages2nd editionTucker and NoonanChapter 18Program CorrectnessTo treat programming scientifically, it must be possible to specify the required properties of programs precisely. Formality is certainly not an end in itself. The importance of formal specifications must ultimately rest in their utility - in whether or not they are used to improve the quality of software or to reduce the cost of producing and maintaining software. J. HorningContents18.1 Axiomatic Semantics18.1.1 Fundamental Concepts18.1.2 The Assignment Rule18.1.3 Rules of Consequence18.1.4 Correctness of the Max Function18.1.5 Correctness of Programs with Loops18.2 Formal Methods Tools: JML18.3 Correctness of Object-Oriented Programs18.4 Correctness of Functional ProgramsMotivationA correct program is one that does exactly what it is intended to do, no more and no less.A formally correct program is one whose correctness can be proved mathematically.This requires a language for specifying precisely what the program is intended to do.Specification languages are based in mathematical logic.Hoare invented “axiomatic semantics” in 1969 as a tool for specifying program behavior and proving correctness.Until recently, correctness has been an academic exercise.Now it is a key element of critical software systems.Correctness ToolsTheorem provers PVSModeling languages UML and OCLSpecification languages JMLProgramming language support Eiffel Java Spark/Ada Specification Methodology Design by contract18.1 Axiomatic SemanticsAxiomatic semantics is a language for specifying what a program is supposed to do.Based on the idea of an assertion:An assertion is a predicate that describes the state of a program at a point in its execution.A postcondition is an assertion that states the program’s result.A precondition is an assertion that states what must be true before the program begins running.A “Hoare Triple” has the form {P}s{Q}{true}int Max (int a, int b) { int m; if (a >= b) m = a; else m = b; fi return m;}{m = max(a, b)}Precondition P: there areno constraints on the inputfor this particular function.Postcondition Q: max is the mathematical idea of a maximum.Program body sPartial correctnessThere is no guarantee that a program will terminate normally. That is, for some inputs, It may enter an infinite loop, orIt may fail to complete its calculations. E.g., consider a C-like factorial function n! whose parameter n and result are int values. Passing 21 as an argument should return n! = 51090942171709440000. But that value cannot be stored as an int, so the function fails. A program s is partially correct for pre- and postconditions P and Q if, whenever s begins in a state that satisfies P, it terminates and computes a result that satisfies Q.Proving Partial CorrectnessProgram s is partially correct for pre- and postconditions P and Q if the Hoare triple {P}s{Q} is valid.There are seven rules of inference that can be used to prove the validity of {P}s{Q}:The Assignment Rule The Sequence RuleThe Skip RuleThe Conditional RuleThe Loop RulePrecondition Consequence RulePostcondition Consequence RuleUsed for basicstatement typesUsed to simplifyintermediatetriplesProof MethodologyA proof is naturally represented as a proof tree.The proof starts with this triple {P}s{Q}. E.g., {true} if (a >= b) m = a; else m = b; fi{m = max(a, b)}An inference is written as , and means “if p and q are valid, then r is inferred to be valid.”Using appropriate rules of inference, break the triple into a group of inferences in which: Each triple is individually valid, and The inferences (logically) combine to form a tree whose root is the program’s original Hoare triple.The Assignment RuleIf Q is a postcondition of anassignment, then replacing all occurrences of t in Q by e is a valid precondition.Examples:The Conditional RuleWe can infer thiswhen wereason backwardsfrom here.E.g.,Rules of ConsequenceE.g.,Precondition strengthening:Postcondition weakening:Correctness of the Max FunctionNote: the assignment rule, the precondition strengthening rule, and the conditional rule are all used in this proof.The Sequence RuleHere, the challenge is to find an Rthat will allow us to break a triple into two valid triples.Notes:The second triple above the line is valid because of the assignment rule.The first triple is valid because both and are valid, using precondition strengthening and the assignment rule. E.g.,The Loop RuleR is called the loopinvariant.The loop invariant remains true before and after each iteration.E.g., inis a good choice for a loop invariant.Note: when the test i < n finally becomes false, the only value for i that satisfies R is i = n, justifying the postcondition {f = n!}Correctness of Programs with LoopsConsider the following triple for a factorial calculation: int f = 1; int i = 1; while (i < n) i = i + 1; f = f * i; odBelow is a sketch of its correctness proof, as two proof trees:part 1 for for the first two statements, and part 2 for the loop.Proof tree for factorial (part 1 of 2)This part uses precondition strengthening, the assignment rule, and the sequence rule.It also establishes the loop invariant as:Proof tree for factorial (part 2 of 2)Notes:The left-hand premise was proved earlier.The right-hand premise is true when the loop terminates. Its validity can be shown mathematically. I.e., if i  n and (i < n) then i = n. But if f = i! and i = n, then f = n!The conclusion follows from the loop rule.Perspectives on Formal MethodsTheory developed in the ‘60s and ‘70sEffectively used to verify hardware designNot widely used in software design, butNew tools are emerging (e.g., JML, Spark/Ada)Techniques have been effective in some critical systems (e.g., the Paris metro system).Many software designers reject formal methods:Too complex for programmersTime better spent with alternative testing methods.Maybe there’s a middle ground?