Lecture 10 (January 27, 1999)

v
Formal
specifications have several interesting properties

Ø
They can play
at least two important and distinct roles

§
They can
provide a basis on which to do verification, ensuring that an implementation
indeed satisfies a specification (you "build the system right")

·
This is
largely the basis for much of the work in program verification, which has not
really succeeded to any significant degree

¨
But it’s the
basis for a bunch of work in this area, and we will cover the basics today

§
They can be
useful in increasing the confidence one has in the consistency and completeness
of a specification

·
For example,
consider the specification of an abstract data type: one can formally check
that the specification of each operation on the ADT guarantees that invariants
on the data itself are satisfied

§
There are
also those who argue for "executable specifications"---that is, specs
that can directly executed or easily translated to executable programs

·
This may work
in some situations, but they are limited because there is a big gap between
either

¨
the
specification and the program (things that are easy to say in a specification
are not necessarily easy to say in programs, especially efficiently ---
negation and conjunction are simple examples)

¨
or else the
user and the specification (reducing the utility of the specification for
helping to ensure that you "build the right system")

Ø
We'll see
some material on specifications based on logic/set theory, on algebra, on
finite state machines

v
Proving
programs correct

Ø
The basic
premise here is that one starts with a specification and a program, with the
job being to demonstrate that the program satisfies the specification

§
A closely
related premise is that one can start with the specification and derive a
correct program from it

Ø
Although
there are many notations that can be used for this process, the two most
well-known ones are Hoare triples and Dijkstra’s weakest preconditions
(predicate transformers)

Ø
A Hoare
triple is a logical predicate of the following form:

§
P {S} Q

·
A common
variant is to write this as {P} S {Q}

§
P and Q are
predicates, while S is a program

§
The meaning
of P {S} Q is

·
If P is true
and S executes

·
Then after S
executes, Q is true

·
Assuming S
terminates

§
The termination
assumption makes this a proof of “weak correctness”

§
If
termination is proven rather than assumed, then it becomes “strong correctness”

§
Ex:

·
true {y :=
x*x} y >= 0

·
x > 0 {x
:= x + 1} x > 1

·
x = X and y =
Y {t := x; x := y; y := t} x = Y and y = X

¨
X and Y are
constants

¨
Note that the
final predicate is not as strong as it could be, since it could also include a
conjunct t = X

·
x <> 0
{if x > 0 then x := x + 1 else x := -x} x > 0

§
These
predicates depend on backsubstitution to capture the meaning of assignment

·
Consider the
triple ? {x := exp} Q(x)

·
? is the
unknown precondition, Q is the postcondition that may be parameterized in terms
of the program variable x

·
For Q(x) to
be true afterwards requires that ? be equal to Q(exp) as a precondition

¨
Q(x) is
defined as x > 1, meaning that Q(x+1) == x+1 > 1 == x > 0

¨
Q(y) == y
>= 0 meaning that Q(x*x) == x*x >= 0 == true

·
This is
handled technically by the proof rule

¨
B[a/X]{X:=a}B

¨
Where B[a/X]
represents the predicate B with all free occurrences of X replaced by a

§
Ex of weak
vs. strong correctness

·
x > 0 { y
:= f(x);

function f(z : int): int is begin

if z=1 return 1

else if even(z) return f(z/2);

else return f(3*z+1);

end }

y = 1

·
I believe
this function has been proven to return 1 if it terminates, but it is only a
conjecture that it always terminates on positive integers

·
Therefore,
this predicate is weakly correct, but not strongly correct

§
We'll come
back to termination proofs, but I do believe that it is relatively rarely the
case where termination is the central issue or problem with a program

·
Also,
demonstrating non-termination is equally important for classes of programs,
such as operating systems, avionics control systems, etc.

Ø
The basic
approach to proving program correct using Hoare triples is as follows

§
One starts
with the precondition (P), the postcondition (Q), and the program (S)

§
S usually
consists of a sequence of statements

§
The person
proving the program then introduces additional intermediate assertions between
the statements

§
Ex:

·
P {S1;S2;S3;S4}
Q

·
P {S1} A1
{S2} A2 {S3} A3 {S4} Q

§
Then prove
each triple. QED.

Ø
Technically,
to do this requires some standard proof rules such as

§
If we can
prove F1{S1}F2 and also F2{S2}F3 then we know that F1{S1;S2}F3 is true

§
If we can
prove that F0 => F1 and the above, as well, we also know F0{S1;S2}F3

Ø
There are
also proof rules for conditional statements, P{if C then S1 else S2}Q

§
If we can
prove

·
P and C {S1} Q

·
P and not C
{S2} Q

·
Then we have
proven the triple P{if C then S1 else S2}Q

§
x <> 0
{if x > 0 then x := x + 1 else x := -x} x > 0

·
P == x
<> 0

Q == x > 0

C == x > 0

x <> 0 and x > 0 == x > 0, so x>0{x:=x+1}x >0, which is
trivially true

x <>0 and x <= 0 == x < 0, so x <0{x := -x}x > 0, which is
also trivially true

QED

Ø
Loops are the
biggest challenge in proving correctness

§
One problem
is proving termination; this is usually done separately from the proof about
the program's computation

§
The other is
that we have to introduce an added assertion, called a loop invariant, and these
are not generally possible to compute, but rather have to be chosen carefully
to allow the proof to go through

§
Consider the
triple P{while C do S}Q

·
We need to
find a loop invariant I and show the following properties

·
P => I //the invariant must
be true when the loop starts

·
I and C{S}I //the invariant must remain
true after each iteration

·
(I and not C)
=> Q //if the loop terminates, the
postcondition must hold

§
Trivial ex
(from Ghezzi):

·
x >= 0 {
while x>0 do x := x + 1 } x = 0

I == x >= 0

P => I trivially

x >= 0 {x := x+1} x >= 0 trivially

x >= 0 and x <= 0 => x = 0 trivially

QED

Ø
Longer
example:

**i > 0 and j > 0**

{t
:= i;

div
:= 0;

while
t >= j do

div := div+1;

t := t-j;

end}

**i =
div*j+t and 0 <= t < j**

** **

§
That is, divide
i by j and put the quotient in div and leave the remainder in t.

§
In groups of
2-4, prove this correct, including explicitly identifying the loop invariant

v
An
alternative formulation to Hoare triples is to use Dijkstra's weakest
precondition predicate transformers that, in essence, provide a functional
approach to handling the predicates

Ø
wp(Q,S) is
defined to be the weakest logical predicate that must be true before executing
S in order to prove that postcondition Q is true afterwards

Ø
Ex:

§
wp(x > 10,x:=x+1)
= x > 9

§
wp(Q,skip) =
Q

§
wp(Q,S1;S2) =
wp(wp(Q,S2),S1)

§
wp(Q, if C
then S1 else S2) = (wp(Q,S1) and C) or (wp(Q,S2) and not C)

Ø
In general,
there is a direct analogy between Hoare triples and wp proofs, although on the
whole, wp proofs seem a little more straightforward, as they seem to capture
the intuitive notion of backwards reasoning for proofs more effectively