What is program verification?
Program verification is the process of providing that
program works correctly for all possible input not just the
ones you test
• Why not just use the testing?
• Testing checks if your program work some
example.
• But it cannot prove your program is always
correct.
• Verification uses math and logic to prove that
your program always give the right result
• To say program is correct we mean:
• 1-it gives the right result .
• 2-it actually finish .
• In this lecture, we foucs only one the frist part
–partial correctness
• Precondition: what must be true before the
code runs.
• Postcondition: what must be true after the
code runs.
• Example
• X=1;
• Y=2; precondition : x=1
• Z=x+y; postcondition :z=3
• Hoare triple
• Cod {postcondition} {precondition}
• This mean :if the preconditionis true ,and the
cod run and end ,then the postcondition will
be true.
• Example: y= 2, z=y+x
• verified because If x=1,then z=1+2=3
• Precondtiton:x=1,postcondition:z+3
Compostion (multiple steps)
You can verify small pieces of code then
combine them.
T=x, x=y, y=t
Precondition:x=7,y=5
Postconditon:x=5,y=7
• Condtion statement (if)
• We must prove:if the condition is true
postcondition after the if
• If the condition is false postcondtion is still true
• If (x>y){y=x;}show that y>=x is always true after
the cod e
• If x>y then y=x so y==x
• If x<=y,noting change stilly>=x
Condition with else
• If (x<0)abs=-x
• Else abs =x
• Postcondition:abs=IxI
• Work because it handies bothe negative and
non –negativex.
Loops and loop invariants
Int i=0; while(i<n){++=i}
Prove i==n after the loop
Loop invariant;i<=n
Each ioopsteps increases iby1 until i==n
Summing and factorial
• sum=0; i=0; while(i<n){
• Sum +=element {i]+=i};
• Loop invariant :sum==total of element
• When loop end i==n so we have added all
element
Egyptian multiplication
• Divide one number by 2 each time ,
• Multiply the other by 2,
• Add only the second number where the first
was odd
• p+a*b==original product
• Thank you