Transcript Correctness proofs presentation

Correctness Proofs
Correctness Proofs
Formal mathematical argument
that an algorithm meets its
specification, which means that
it always produces the correct
output for any permitted input.
Correctness Proofs
Is Important to understand
what a deteiled formal
correctness proof looks like,
because otherwise you won’t
know what somebody is really
saying with an informal
correctness argument.
Invariants, Preconditions and
Posconditions.
1.
2.
3.
P holds in the initial state.
P holds after step k if it hods
before step k.
If P holds when the algorithm
terminates, then the output of
the algorithm is correct.
Hoare Logic
 Attach
to each statement of a
program a precondition and a
postcondition.
 Precondition,
Statement and
Postcondition, form a Hoare
triple.
Hoare Logic
{ x is even }
x := x + 1
{ x is odd }
{ P: x is an integer }
x := 2*x
{ Q: x is even }
x := x+1
{ x is an integer }
{R: x is odd }
x := 2*x
{ x is even }
Hoare Logic
{P} S1 {Q} Λ {Q} S2 {R}
{P} S1:S2 {R}
Composition Axiom
Hoare Logic Axioms
Rules like before, which
define what new
propositions can be
deduced from old ones,
are called Axioms.
Pre-strengthening Axiom
Making the precondition stronger
doesn’t change the truth of a
Hoare triple.
{Q} S {R} Λ P  Q
{P} S {R}
Pre – strengthening Axiom
Mostly used to sneak in extra
facts that don’t appear explicitly
in our original precondition.
If whenever Q is true,
PPΛQ
is also true.
Post – weakening Axiom
Making the postcondition
weaker is also allowed.
{P} S {Q} Λ Q  R
{P} S {R}
Post – weakening Axiom
Typically used for getting rid of
bits of a postcondition we don’t
care about.
The direction of the implications
is important. Pre – weakening
and post – strengthening do
NOT produce valid proofs.
Assignment Axiom
{P[x/t]} x := t {P}
If P is true with x replaced by t before
the assignment, it is true without the
replacement afterwards.
{0 = 0} x := {x=0}
{x+5 < 12} x:= x+5 {x < 12}
{x < 7} x:= x+5 {x < 12}
Baggage Lemma
Used to carry along extra baggage
that you will need later.
{ } S {x = A}
But you also need know that y is
unchanged.
{y = B} S {y = B Λ x = A}
Strategy
1.
Write down the algorithm.
2.
Precondition and postcondition
for each statements.
3.
Prove for each statement that
its postcondition follow from its
precondition.
Proofs for if/then/else statements
{P}
if B then
{P and B}
do something
{Q}
else
{P and Not B}
do something
{Q}
end if
{Q}
Proofs for if/then/else statements
{P Λ B} S1 {Q} Λ {P Λ ¬B} S2 {Q}
{P} if B then S1 else S2 end if {Q}
Proofs for Loops
{P}
while B do
{R and B}
body
{R}
end while
{Q}
Proofs for Loops
{A is an array with indices 0..n-1}
i := n
While i <> 0 do
{A[j] = 0 for all j >= i}
i := i – 1
{A[j] = 0 for all j >= i+1}
A[i] := 0
{A[j] = 0 for all j >= i}
end while
{A[0] .. A[n-1] are all equal to zero}
Total vs Partial Correctness
We will want to show that an
algorithm produce the right
output in a reasonable amount
of time, tipically bounded by
some function of the size of
the input.
Proofs for Recursive Procedures
Procedure Euclid(x,y: integer) return integer
{}
if y = 0 then
{y = 0}
gcd := x
{gcd = gcd(x,y)}
else
{y <> 0}
gcd := Euclid(y,x mod y)
{gcd = gcd(x,y)}
endif
{gcd = gcd(x,y)}
return gcd
end procedure
{return value = gcd(x,y)