Publish on 04th November 2019
Category: Birds
0

Designing Programsthat Check Their Work

Manuel BlumSampathKannan

by Jeffrey Corbell

Overview

Introduction to a Program CheckerOther Methods of Determining CorrectnessDefinition of a Program CheckerExample of a Checker: Graph IsomorphismBeigel’s Theorem

What is a program checker

Program that checks the output of a program to determine if the program is correct or buggyFormally:P and C are programs, I is the inputFor any I run on P, C is run and determines whether P is correct for I or buggy

Other Methods of Determining Correctness

Program verificationUse a proof to prove a program is correctVery difficult to doArgued that it doesn't improve confidence in correctnessvery complexmay contain errors which would be difficult to detect

Other Methods of Determining Correctness

Program testingRun program on input that you know the correct output forCompare program output to expected outputProblemsNo general way to create test dataNo theorems to describe behavior if they do pass tests

Differences Between a Checker and Testing

A checker is a program that uses its own algorithm that allows it to check the outputProgram testing usually only uses a small amount of predetermined cases for specific input

Definition of a Bug

Letπrepresent a decision or search problemxrepresents an input toπwithπ(x) representing the outputPis a deterministic program that supposedly solvesπP has a bug if for some instancexofπP(x) ≠π(x)

Definition of a Checker

LetCπbe the checker,kbe the number of different cases the checker tries, andIbe the group of test inputsCπP(I,k) is the output of the checker and follows these conditions:1. IfP(x) =π(x), then with probability ≥ 1- 1/2kCπP(I,k) =CORRECT2. IfP(x) ≠π(x), then with probability ≥ 1- 1/2kCπP(I,k) =BUGGY

Definition of a Checker

However, ifPhas bugs butP(I)=π(I) thenCπP(I,k) may output eitherCORRECTorBUGGY

Definition of a Checker

AssumedPhalts on all inputsNot always the caseIfP(x) exceeds a predetermined bound then the checker should raise a flag,CπP(I,k) =TIME

Definition of a Checker

Runtime includes the time it takes to submit input and receive output fromPDoes not include the time it takesPto run

Definition of a Checker

If a checker is a program, how can you be sure the checker is correct?You can’t reallyChecker must have thelittle ohproperty with respect to the runtime ofPEnsures the checker is programmed differently than the original program

Graph Isomorphism

b

e

a

c

d

1

2

4

3

5

f(a) = 1f(b) = 2f(c) = 3f(d) = 4f(e) = 5

Graph Isomorphism Checker

LetPbe a program that solves graph isomorphismInput: two graphs G and HOutput:YESif G is isomorphic to H;NOotherwise

CGIP(G, H,k) checksPon input G and H

Graph Isomorphism Checker

ComputeP(G,H)IfP(G,H)=YESthenUsePto search for an isomorphism from G to HCheck if the resulting correspondence is an isomorphismIf not, returnBUGGY; if yes, returnCORRECT

Graph Isomorphism Checker

IfP(G,H)=NOthenDoktimes:Toss a fair coinIf coin = heads thenGenerate a randompermutation G’ of GComputeP(G,G’)IfP(G,G’)=NOthen returnBUGGY

If coin = tails thenGenerate a random permutation H’ of HComputeP(G,H’)IfP(G,H’)=YESthen returnBUGGY

ReturnCORRECT

Graph Isomorphism Checker

CGIPruns in polynomial timeIfPhas no bugs and G is isomorphic to H, then CGIP(G,H,k) creates an isomorphism from G to H and outputsCORRECTIf P has no bugs and G is not isomorphic to H, then CGIP(G,H,k) tosses coins. It discoversP(G,G’)=YES for all G’ andP(G,H’) for all H’ so outputsCORRECT

Graph Isomorphism Checker

IfP(G,H) is incorrect then there are two cases:IfP(G,H)=YESbut G is not isomorphic to H, then CGIPfails to construct an isomorphism and outputsBUGGYIfP(G,H)=NObut G is isomorphic to H, the only way that C will returnCORRECTis if P(G,G’)= YES if the coin is heads and P(G,H’)= NO when it is tails. But G and H are permuted randomly to produce G’ and H’. Therefore P correctly distinguishes G’ from H’ only by chance for just 1 of 2kpossible sequences

Beigel’s Theorem

Letπ1andπ2be two polynomial-time equivalent decision problems. Then from any polynomial time checker forπ1it is possible to construct a polynomial-time checker forπ2.

Beigel’s Theorem

Have a checker Cπ1forπ1and a programP2forπ2Also have two way polynomial time transformationsf1,2andf2,1This gives us a program forπ1P1(x) =P2(f1,2(x))

Beigel’s Theorem

To checkP2on an inputy, computeP2(y) then transform into an inputzforπ1usingf2,1Then use Cπ1to checkz.Any call Cπ1makes toP1is transformed to a call toP2

P2

Cπ1

f1,2

f2,1

y

z

P1

Beigel’s Theorem

If P2is correct then P1will be correct because P1is defined in terms of P2Thus if P1is correct onzthen P2is correct onyIf P2is wrong onyand P1is correct onzthen there’s a contradiction because P2(y)=P1(z)If P1is wrong onzthen the checker Cπ1will catch it

Beigel’s Theorem

This checker forπ2runs in polynomial timeRunning the checker forπ1One transformation off2,1Polynomial number of applications off1,2

Bibliography

Designing programs that check their work - M. Blum and S. KannanSocial Processes and Proofs of Theorems and Programs - R.A. De Millo, R.J. Lipton, and A.J. Perlis.Introduction to the Theory of Computation– M. Sipserwww.wikipedia.org

0

Embed

Upload

Designing Programs that Check Their Work - cs.ucf.edu