Transcript ch01s6

Formal Logic
Mathematical Structures
for Computer Science
Chapter 1
Copyright © 2006 W.H. Freeman & Co.
MSCS Slides
Formal Logic
Proof of Correctness






Section 1.6
Program verification attempts to ensure that a computer
program is correct.
A program is correct if it behaves in accordance with its
specifications.
This does not necessarily mean that the program solves the
problem that it was intended to solve; the program’s
specifications may be at odds with or not address all aspects of a
client’s requirements.
Program validation attempts to ensure that the program indeed
meets the client’s original requirements.
Program testing seeks to show that particular input values
produce acceptable output values.
Proof of correctness uses the techniques of a formal logic
system to prove that if the input variables satisfy certain
specified predicates or properties, the output variables produced
by executing the program satisfy other specified properties.
Proof of Correctness
1
Assertions





Section 1.6
Let us denote by X an arbitrary collection of input values to
some program or program segment P.
The actions of P transform X into a corresponding group of
output values Y.
The notation Y = P(X) suggests that the Y values depend on
the X values through the actions of program P.
A predicate Q(X) describes conditions that the input values
are supposed to satisfy. Q is the precondition.
A predicate R describes conditions that the output values are
supposed to satisfy. These conditions will often involve the
input values, so R has the form R(X, Y) or R[X, P(X)]. R is
the postcondition.
Proof of Correctness
2
Assertions



For example, if a program is supposed to find the square
root of a positive number, then X consists of one input
value, x, and Q(x) might be “x  0.”
If y is the single output value, then y is supposed to be the
square root of x, so R(x, y) would be “y2 = x.”
Program P is correct if the following implication is valid:
("X)(Q(X)  R[X, P(X)])
For the square root case, it is:
("x)(x > 0  [P(x)]2 = x )
The traditional program correctness notation (called a
Hoare triple) is:
{Q}P{R}





Section 1.6
Proof of Correctness
3
Assertions


A program or program segment is broken down into individual
statements si, with predicates inserted between statements as well as at
the beginning and end.
These predicates are also called assertions because they assert what is
supposed to be true about the program variables at that point in the
program.

{Q}
s0

{R1}
s1

{R2}
s n 1
.
.
.


Section 1.6
{R}
Where Q, R1, R2, ... , Rn = R are assertions. The intermediate assertions
are often obtained by working backward from the output assertion R.
Proof of Correctness
4
Assertions

P is provably correct if each of the following
implications holds:






Section 1.6
{Q}s0{Rl}
{Rl}sl{R2}
{R2}s2{R3}
.
.
.
{Rn1}sn1{R}
A proof of correctness for P consists of producing this
sequence of valid implications.
Some new rules of inference can be used, based on the
nature of the program statement si.
Proof of Correctness
5
Assignment Rule





Section 1.6
Suppose that statement si is an assignment statement of the
form x = e for some expression e.
The Hoare triple to prove correctness of this one statement has
the form: {Ri} x = e {Ri + l}.
For this triple to be valid, the assertions Ri and Ri +1 must be
related in a particular way.
The appropriate rule of inference for assignment statements is
the assignment rule.
It says that if the precondition and postcondition are
appropriately related, the Hoare triple can be inserted at any
time in a proof sequence without having to be inferred from
something earlier in the proof sequence. It has the following
conditions:
1. si has the form x = e.
2. Ri is Ri + 1 with e substituted everywhere for x.
Proof of Correctness
6
Assignment Rule

For example, the Hoare triple:
{x  1 > 0} x = x  1 {x > 0}
is valid by the assignment rule.
The postcondition is:





Substituting x  1 for x throughout the postcondition
results in:


Section 1.6
x>0
x – 1 > 0 or x > 1
which is the precondition.
Proof of Correctness
7
Conditional Rule



A conditional statement is a program statement of the form:
if condition B then
P1
else
P2
end if
A conditional rule of inference determines when a Hoare triple
can be inserted in a proof sequence if si is a conditional
statement.
The Hoare triple is inferred from two other Hoare triples:



Section 1.6
{Q /\ B} P1 {R} if B is true
{Q /\ B} P2 {R} if B is false
This simply says that each branch of the conditional statement
must be proved correct.
Proof of Correctness
8
Conditional Rule

For example:


We must prove:




Section 1.6
{n = 5 and n >= 10} y = 100 {y = 6}
{n = 5 and n < 10} y = n + 1 {y = 6}
Using the assignment rule we get:


{n = 5}
if n >= 10 then
y = 100
else
y=n+1
end if
{y = 6}
{n = 5} y = n + 1 {y = 6}
{n = 5 and n < 10} y = n + 1 {y = 6}
The conditional rule allows us to conclude that the program
segment is correct.
Proof of Correctness
9