, we may have
.
States may be modified by actions that result from
executing the program, such as by an assignment
of a value to a variable.
We employ substitutions to modify a state.
As before, substitutions may be defined by an equation, as
given in slide 10-subst.
states that modifying 
by
assigning the value v to the variable x
then, for a variable y, the state 
will
deliver v whenever y is identical to x and 
otherwise.
When we have, for example, an assignment 
then we have as the corresponding transition
where 
,
that is 
is like 
except
for the variable i for which the value 5
will now be delivered.
Whenever we have a sequence of actions 
then, starting from a state 
we have corresponding
state transformations resulting in states
as intermediary states and
as the final state.
Often the states 
and 
are referred to
as respectively the input and output state
and the program that results in the actions 
as the state transformer modifying 
into 
.
where S denotes a program (fragment)
and P and Q respectively the pre-condition
and post-condition associated with S.
A formula of the form 
is true if, for every
initial state 
that satisfies P and for which
the computation characterized by S terminates,
the final state 
satisfies Q.
This interpretation of 
characterizes partial correctness, partial since
the truth of the formula is dependent on the termination of
S (which may, for example, for a while statement,
not always be guaranteed).
When termination can be guaranteed, then we
may use the stronger notion of total correctness,
which makes the truth of 
no longer dependent on the termination of S.
Pre- and post-conditions may also be used to check
invariance properties.
As an example, consider the following
correctness formula:
It states that the begin and end state of the
computation characterized by 
is invariant with respect to the condition 
.
As an exercise, try to establish the correctness of
this formula!
To verify whether for a particular program fragment
S and (initial) state 
satisfying P
the correctness formula 
holds,
we need to compute the (final) state 
and check that Q is true for 
.
In general, for example in the case of non-deterministic
programs, there may be multiple (final) states
resulting from the execution of S.
For each of these states we have to establish that
it satisfies (the post-condition) Q.
We call the collection of possible
computation sequences of a program fragment S
the traces of S.
Traces characterize the (operational) behavior
of a program.
and
the requirement 
.
Applying the assignment axiom we have 
.
Consequently, when we are able to prove that P implies 
,
we have, by virtue of the first consequence rule, proved that
.
The next rule, for sequential composition, allows
us to break a program (fragment) into parts.
For convenience, the correctness formulae for multiple
program fragments that are composed in sequential order are
often organized as a so-called proof outline of the form
.
When sufficiently detailed, proof outlines may be regarded
as a proof.
For example, the proof outline
constitutes a proof for the invariance property discussed earlier.
Clearly, the correctness formula for the two individual components
can be proved by applying the assignment axiom.
Using the sequential composition rule, these components
can now be easily glued together.
As a third rule, we have a rule for conditional statements of the form
.
As an example, consider the correctness formula
.
All we need to prove, by virtue of the inference rule
for conditional statements, is that 
which (again) immediately follows from the assignment axiom.
As the last rule for proving correctness, we present here
the inference rule for iterative (while) statements.
The rule states that whenever we can prove that a certain
invariant I is maintained when executing the body of
the while statement (provided that the condition b is satisfied)
then, when terminating the loop,
we know that both I and 
hold.
As an example, the formula
) i--;
trivially follows from the while rule by taking I to be true.
Actually, the while rule plays a crucial role in constructing
verifiable algorithms in a structured way.
The central idea, advocated among others by 
then we may, by simultaneously applying the two consequence rules,
derive the formula
which amounts to strengthening the pre-condition
and weakening the post-condition.
The intuition justifying this derivation
is that we can safely promise less and require more,
as it were.
Finally, the rule most important to us in the present context
is the inference rule characterizing correctness
under procedural abstraction.
Assuming that we have a function m with formal parameter x
(for convenience we assume we have only one parameter, but this
can easily be generalized to multiple parameters), of which
the (function) body consists of 
.
Now, moreover, assume that we can prove for an arbitrary expression
e the correctness formula 
,
with e substituted for the formal parameter x in both
the conditions and the function body, then we also have
that 
, provided
that P and Q do not contain references to local variables
of the function m.
In other words, we may abstract from a complex program fragment
by defining a function or procedure
and use the original (local) correctness proof
by properly substituting actual parameters for formal parameters.
The procedural abstraction rule, which allows us
to employ functions to perform correct operations,
may be regarded as the basic construct needed to verify
that an object embodies a (client/server) contract.
|
Hush Online Technology
hush@cs.vu.nl
12/29/99 |
|
|