Follow
Publications: 120 | Followers: 1

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

Publish on 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

Share

Upload

Make amazing presentation for free
Designing Programs that Check Their Work - cs.ucf.edu