Transcript Program Proving Notes

Program Proving Notes
Ellen L. Walker
Formal Specification & Proof
of Programs (Verification)
– Formally proving that a program satisfies a
formal specification
– Alternative to testing to determine whether
a program works as specified.
– One means of specifying program
semantics
Definitions
– Specification — description of what a program should do,
usually in English.
– Formal specification — a specification using formal
mathematical notation. Mathematical notation makes the
specification more concise & more precise.
– Proving (verifying) a program — given a program and a
formal specification, use formal proof techniques (e.g.
induction) to prove that the program behavior fits the
specification.
– Specification of a programming language (semantics) —
formal specification for each statement in the language.
Formally Proving a Program
– Given:
• formal specification of program
• specification of programming language
• a program in the language
– Prove:
• the program executes according to
specifications
Conditions in Specification
• Preconditions
– Must hold before the program executes
• Postconditions
– Must hold after the program executes
A formal specification always has both
preconditions and postconditions
Notation
• P{S}Q
– P is the precondition
– S is the program (or statement)
– Q is the postcondition
• P and Q are written in logic
• S is written in the programming
language (or pseudocode)
Specification as Logic
• (P and execution of S) -> Q
• If this expression is always true we say
the specification is valid
Example
• x > 0 { x = -x } x < 0
– Precondition: x>0
– Postcondition: x<0
– Program: x = -x
• This specification is valid
– When the precondition holds before the
program, the postcondition will always hold
after the program.
Special Cases
• P { S } true
– Valid for all programs and preconditions
• false { S } Q
– Valid for all programs and postconditions
– When the precondition is false before
program runs, the specification is valid no
matter what!
Many Choices for P and Q
• true { y = x + 1} y > x
• x > 0 { y = x + 1} y > x
• x = 1 { y = x + 1} y > x
• x = 1 { y = x + 1} true
• x = 1 {y = x + 1} y > x
• x = 1 {y = x + 1} y > 1
• x = 1 {y = x + 1} y = 2
Logical Implication
• P->W (“P implies W” or “If P then W”)
P
W
P->W
True
True
True
True
False
False
False
True
True
False
False
True
Mathematical examples
•
•
•
•
•
•
(a>b) -> (b < a)
true
(a≥b) -> (a > b)
false
(a>b) -> (a ≥ b)
true
(a>b) -> (a > b+1)
false
(a>b) -> (a ≥ b+1)
false
(a>b) and a and b are integers -> (a≥b+1)
true
Rules of Implication
•
•
•
•
•
•
Shorthand: “a->b” means “a->b is true”
(A and B) -> A
(A and B) -> B
A -> (A or B)
B -> (A or B)
(A->B) is equivalent to (not B -> not A)
Strength of Conditions
• If P1 and P2 are conditions,
and P1 -> P2,
• Then P1 is stronger than P2
and P2 is weaker than P1
• Intuition: stronger conditions are more
specific, have fewer “possibilities”
Strength of Conditions
(continued)
• The strongest possible condition is false
– False -> Q for all Q
• The weakest possible condition is true
– P -> True for all P
• Not all conditions are comparable
– (y > 1) is not comparable to (x > 0)
– (y > 5) is not comparable to (y < 8)
• No implication either way
Weakest Precondition
– Many choices for Precondition
• true { y = x + 1} y > x
• x > 0 { y = x + 1} y > x
• x = 1 { y = x + 1} y > x
– Choose the weakest for best
specification
• Avoids “unnecessary” specification
Why Weakest Precondition?
• Suppose P and W are preconditions and
P->W (W is weaker)
– Given W { S } Q and P true before the program
begins
– Because P->W, W is also true before the program
begins
– Therefore P { S } Q
• “W is the precondition that implies all other
preconditions that allow S to run and
guarantee Q as a postcondition”
• Notation: W = wp(S, Q)
Proving a Program
Specification
Goal: prove P { S } Q
1. Find wp(S,Q)
2. Prove that P -> wp(S, Q)
Work backwards from postcondition to
precondition
Example
•
•
•
•
Prove k>0 {x = 1/k } xk=1
wp(x=1/k,xk=1) is k≠0
(k>0) -> (k≠0) for all k
Therefore, our specification is true.
More Examples
– Prove x = 1 {x = 1/x} x > 0
• wp (x = 1/x, x > 0) is 1/x > 0, or x > 0
• Since 1>0, x=1 implies x > 0
• Therefore, the specification x =1 {x = 1/x} x > 0 is true.
– Prove x ≠ 0 {x = x + 1} x > 0
• wp (x= x + 1, x > 0) is x' + 1 > 0 or x' > –1
• x ≠ 0 doesn't necessarily imply x > –1 (consider x = –5)
• Therefore, the specification x ≠ 0 {x = x + 1} x > 0 is false
Programming Language
Semantics
• Language consists of Statements
• Complex statements derived from
simpler statements and control
structures
– Conditionals (IF)
– Loops (WHILE)
A Small Language
1.
2.
3.
4.
5.
Empty statement (skip)
Assignment statement (x=y)
Sequence of statements ( { S1 S2 } )
Conditional ( if (C) S1 else S2 )
Loop ( while (C) S )
Specifying Language
Semantics
• For each statement, determine the wp
of the statement
• Statement wp depends on its parts
– Using conditions (C) directly
– Using wp of subordinate statements (S)
Semantics of skip
• The empty statement has no effect
• Therefore wp(skip, Q) is Q
• Example: wp(skip, x<0) is x<0
Semantics of Assignment
• Given x = E (where E is an expression)
• Two cases:
– Postcondition does not contain x
• Wp(x=E,Q) = Q because Q is unaffected
– Postcondition does contain x
• Consider Q as a function of x
• Wp(x=E, Q(x)) = Q(E)
• To be careful, we must add “and E is defined”
to avoid cases such as x = 1/0
Assignment Examples
• Wp (x=y, y>5) is y>5
– Q does not contain x
• Wp (x=y, x<2) is y<2
– Q does contain x, so substitute y for x
• Wp (x = x+1, x>4) is x’>3
– Use x’ as the “before” value of x
Assignment vs. Equality Test
• Be careful
– x=0 {x=1} x=1
Semantics of a Sequence
• Given P {S1} R and R {S2} Q, we can
write P { {S1 S2} } Q
• Therefore
– Wp({S1 S2}, Q) = wp(S1, wp(S2, Q))
• Find wp of the second statement and
the postcondition (R, above)
• Then find wp of the first statement with
that wp (R) as the postcondition
Examples
• wp ({x=y; x= 1/x;}, x>0) is
wp(x=y, wp(x=1/x, x>0)) is
wp(x=y, 1/x > 0) is wp(x=y, x>0) is
y>0
• wp({x = 2*t; skip;}. x>5) is
wp(x=2*t; wp(skip, x>5)) is
wp(x=2*t, x>5) is
2t > 5 is t > 2.5
One More Example
• true {x = 5; y = 2; x = x*y} x=10
Semantics of IF
• The conditional with test T and statements S1
and S2 is
– if (T) S1 else S2
– When there is no “else, write: if (T) S1 else skip
• Wp(if (T) S1 else S2) is
(T and wp(S1,Q)) or ((not T) and wp(S2,Q))
– If T is true, use S1’s precondition
– If T is false, use S2’s precondition
• Equivalently,
(T-> wp(S1,Q)) and ((not T)-> wp(S2,Q))
Proving a Loop
• Two things to prove
– If the loop terminates, the postcondition is
true
– The loop terminates
• Proving only the postcondition is called
weak correctness
Weak Correctness Example
• True {while true x=1} x=1
• Weakly correct
– If the loop ever terminated, x would be 1
• Not strongly correct
– But the loop will never terminate
Semantics of WHILE
• Treat as a “repeated if”, where B must be true
the last time
• Define Pk = wp(loop executes k times, Q)
• wp(while (B) S, Q)
–
–
–
–
P0 = Not B and Q
P1 = B and wp(S, P0)
P2 = B and wp(S, P1)
Pk = B and wp(S, Pk-1)
• wp(while (B) S, Q) = P0 or P1 or P2 or… Pk
How to Solve the Infinite OR
• Direct approach
– Use mathematics to solve the infinite
series
– Nice if it works, but you have to see the
pattern
• Indirect approach
– Prove weak correctness and termination
separately
– Use “loop invariant”
Example: Direct Proof
• What is wp(while (i<n) i=i+1, i=n) ?
– H0 : not B and Q
• not(i<n) and i=n
• i=n
– H1: B and wp(S, H0)
• i<n and wp(i=i+1,i=n)
• i<n and i+1=n
• i+1=n
Direct Proof, continued
– H2: B and wp(S,H1)
• i<n and wp(i=i+1,i+1=n)
• i+2=n
– Hk: B and wp(S,Hk-1)
• i<n and wp(i=i+1,i+k-1=n)
• i+k=n
• H0 or H1 or H2 or H3 or …
• i=n or i+1=n or i+2=n or … i+k=n …
– The above is equivalent to writing i≤n
Loop Invariants
(Indirect method)
• A loop invariant is any statement that is true
every time a loop executes.
• For example, consider the fragment:
i = 1; x = 1;
while (i < n ) {
x = x * i;
i = i + 1;
}
• One invariants is: i<n (or the loop ends)
A Loop has Many Invariants
• 3 different invariants for the example loop:
– i < n (because the loop will terminate if i ≥ n)
– true (an invariant of every loop)
– x = (i – 1)! (because x started at 1 and has been
multiplied by 1, 2, 3 ... i
• This last invariant is most useful: it tells what
the loop does.
Using Loop Invariants to
Prove Weak Correctness
•
Prove P { while B S} Q
1. Invariant is true after each time S runs
B and inv {S} inv
2. When the loop ends, Q is true
(Not B and inv) -> Q
3. Invariant is true before the loop
P -> inv
Example Loop
i = 1 and x = 1 and n > 0 //pre
{
while ( i < n ) {
x = x * i;
i = i + 1;
}
}
x = (n – 1)! //post
• Prove, using inv: 0< i ≤ n and x = (i –1)!
Step 1
• B and inv {S} inv
• B and inv is: (i<n) and 0< i ≤ n and x = (i –1)!
, or 0<i<n and x=(i-1)!
• Wp(S, inv) is:
Wp((x=x*i, i=i+1), 0<i≤n and x=(i-1)!) =
Wp(x=x*i, wp(i=i+1, 0<i ≤ n and x=(i-1)!)) =
Wp(x=x*i, 0<i+1 ≤ n and x=(i!))
0<i+1 ≤ n and x*i = i!
-1<i ≤ n-1 and x = (i-1)!
(since i is integer, we know that -1< i < n)
• B and inv -> wp(s, inv), so step 1 is complete
Step 2
• Not B and inv -> Q
(i>= n) and (0< i ≤ n and x = (i –1)! ) is
i = n and x = (i-1)!
x = n-1!
• The above expression is Q, so Step 2 is
complete
Step 3
• P -> inv
– P is: i=1 and x=1 and n>0
– Since n>0 and i=1, 0<I ≤ n
– We define 0! = 1. Since x=1 and i=1,
x=(i-1)!
• Both parts of the invariant are proven,
so Step 3 is complete
Finding the Invariant
• Invariant is an approximation to the
weakest precondition
• Find it by working the loop body
backwards, treating inv as a function
with loop variables as parameters
– Wp(inv(params), S) = B and inv(params)
• Your first guess is often too weak (it’s an
invariant but won’t prove the loop)
Example
Find an invariant for the loop
while (i < n) {
i = i + 1;
x = x * i;
}
Note: the invariant also “explains” the loop
Proving Termination
• Somehow, we need to make an
argument that:
– The loop ends when B becomes false
– Each iteration gets us “closer” to B
becoming false
• Formally, this is done using a “wellfounded set”
Well-Founded Set
• An ordered set with a “bottom element”
• Any decreasing sequence in the set must
reach the “bottom element” with a finite
number of elements
• Examples:
– [0-99]
– Non-negative integers
– Letters of the alphabet (bottom is “a”)
Proving Termination using
WFS
• Find a well-founded set such that:
– Every loop execution generates an
element of the set (e.g. value of n-I)
– If the bottom element is reached, the loop
terminates (e.g. n-I becomes 0 when I=n)
– The sequence of values generated through
multiple iterations of the loop is decreasing
(e.g. since I gets bigger, n-I gets smaller)
Summary
• Axiomatic semantics allows any program in
the language to be proven correct
• In the specification of a language, the
weakest precondition for each statement type
must be defined
• Loops can be proven directly using an OR of
weakest preconditions, or indirectly using an
invariant and a separate proof of termination