φ
slide: Substitution
A substitution
φ
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
φ(y)
otherwise.
When we have, for example, an assignment
φ(y)
then we have as the corresponding transition
φ−i=5 → φ′
where
φ−i=5 → φ′,
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
φ0 we have corresponding
state transformations resulting in states
φ1,…,φn−1 as intermediary states and
φ1,…,φn−1 as the final state.
Often the states
φ0 and
φn are referred to
as respectively the input and output state
and the program that results in the actions
φn
as the state transformer modifying
φ0 into
φ0.
- φ
- operations a1,a2,…,an
- φi \apijla φj ∧φi \models P ⇒ φj \models Q
slide: The verification of state transformations
To characterize the actions that result from
executing a program, we need an operational semantics
that relates the programming constructs to
the dynamic behavior of a program.
We will study such a semantics in section \ref{10:behavior}.
The requirements a program (fragment)
has to meet may be expressed by using predicates
characterizing certain properties
of a program state.
Then, all we need to do is check whether the final state
of a computation satisfies these requirements.
Predicates characterizing the properties of a state
before and after executing a program (fragment)
may be conveniently stated by
correctness formulae of the form
{P} S {Q}
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
{P} S {Q} 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
{P} S {Q}
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:
{P} S {Q}
It states that the begin and end state of the
computation characterized by
i = i + 1; s = s + i
is invariant with respect to the condition
i = i + 1; s = s + i.
As an exercise, try to establish the correctness of
this formula!
To verify whether for a particular program fragment
S and (initial) state
i = i + 1; s = s + i satisfying P
the correctness formula
i = i + 1; s = s + i
holds,
we need to compute the (final) state
i = i + 1; s = s + i
and check that Q is true for
i = i + 1; s = s + i.
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.