Copyright © 2000 by Rex Page 11AutomatedMathematical Induction2Principle of Mathematical Induction{∀I} — an inference rulewith ∀n. P(n) as it’s conclusionP(0) ∀n.P(n)→P(n+1)⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯{Ind}∀n. P(n)InductionOne way to use {∀I} Prove P(0) Prove P(n +1) for arbitrary n9 Takes care of P(1), P(2), P(3), … Mathematical induction makes it easier Proof of P(n +1) can cite P(n) as a reason9 If you cite P(n) as a reason in proof of P(n+1),your proof relies on mathematical induction9 If you don’t, your proof relies on {∀I}P(n) {n arbitrary}⎯⎯⎯⎯⎯⎯⎯⎯⎯{∀I}∀n. P(n)∀ Introduction3Axioms about Sequences Algebraic laws of sequence construction[]: list[ _|_] : int, list -> list Informally [ x | [x1, x2, …] ] = [x, x1, x2, …] Definition of concatenationcons: list, list -> listcons([ ], ys) = ys (1)cons([x | xs], ys) = [x | cons(xs, ys)] (2) Definition of lengthlength: list -> integerlength([]) = 0 (3)length([x | ys]) = 1 + length(ys) (4) Can we prove the following?length(cons(xs, ys)) = length(xs) + length(ys) (5)Copyright © 2000 by Rex Page 24 Prove ∀xs. P(xs)where P(xs) ≡ ∀ys. length(cons(xs, ys)) = length(xs) + length(ys) Inductive case: P(xs) → P(x: xs)Example: Concatenation Conserves LengthAssume concatenation (cons), and length satisfycons([ ], ys) = ys (1)cons([x | xs], ys) = [x | cons(xs, ys)] (2)length([]) = 0 (3)length([x | ys]) = 1 + length(ys) (4)length(cons([x | xs], ys)= length([x | cons(xs, ys)) {(2)}= 1 + length(cons(xs, ys)) {(4)}= 1 + (length(xs) + length(ys)) {induction hypothesis, P(xs) }= (1 + length xs) + length ys {+ assoc}= length([x | xs]) + length(ys) {(4) backward}length(xs) → integer Base case: P( [ ] ) { uses (1) and (3)}5Software Examples sum times gcd length cons reverse maximum vector addition insertion sort merge merge sort quick sort exponentiation binary tree search circuit boards compilers operating systems Boyer and Moore’s Computational Logic SystemWritten in lisp and prove properties of lisp programs Significant properties verified9 Lots of examples in reasoning about software9 Supporting reasoning tools are needed:9Simplification: rewriting9Deduction: resolution6ApplicationsMathematical proof checkingThe QED ProjectComputer chip verificationsSoftware verificationCopyright © 2000 by Rex Page 37Mathematical Proof CheckingAutomated theorem proversdo not “automate” math“Debugs” proofsHard to use many proof checkers8The QED ProjectEffort of scientists from many laboratories and institutions“The development of mathematicstowards a greater appreciation has led... to the formalization of large tracts of it, so that one can prove any theorem using nothing but a few mechanical rules.”-K.Gödel••Will represent Will represent mathematical mathematical knowledge, techniqueknowledge, technique••Based on a few pages Based on a few pages of mathof math••Still in early stagesStill in early stages9The QED Project- Hoped BenefitsReduce mathematical “noise pollution.”Speed publication of papers by taking focus off of proof checking. Referees can focus on relevance.Cultural monument to mathematics.Copyright © 2000 by Rex Page 410Chip VerificationFormal vs.testbenchComparison verificationNP-CompleteIBM, Intel, AMD successes11Software VerificationHardware is more economically viableMore design effort put into software=> Software verification is viableEspecially useful for critical applications: safety, e-commerce, military12Software Verification ParadoxWhat will verify the verification program?Pragmatism does not demand ideal accuracySignificant improvement
View Full Document
Unlocking...