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