1. Introduction
The idea of using a single formula to represent the behaviour of a program is a very attractive one: proving that two programs are equivalent then reduces to the task of proving that two formula are equivalent. For the latter task, mathematicians have developed many powerful techniques over the last few thousand years of the history of mathematics.
In this paper, we show that a single formula is insufficient to represent the semantics of a program in the de- sired way, but there are two formulae which are sufficient.
2. The WSL Language
The WSL transformation theory is based in infinitary logic: an extension of first order logic which allows infi- nitely long formulae. The statements in the WSL kernel language are as follows:
is an assertion which terminates immediately if
is true and aborts if
is false,
is a guard which ensures that
is true without changing the value of any variable,
adds the variables in
to the state space, if they are not already present, and assigns arbitrary values to the variables.
removes the variables in
from the state space,
is sequential composition,
is nondeterministic choice, and
is a recursive subroutine which also adds the variables in
to the state space and removes the variables in
from the state space.
The semantics of a WSL program is defined as a function which maps each initial state to the set of possible final states. A state is either the special state
, which represents non-termination, or a proper state which is a function from a set of variables (the state space) to the set of values. The semantics of a program is always de- fined in the context of a particular initial state space and final state space.
For any list of variables
, we define
to be the set of variables in
, and
and
to be the cor- responding sequences of primed and doubly primed variables. The formula
is true precisely when the value of any variable in
differs from the value of the corresponding variable in
.
The interpretation function
maps each statement
and initial state space
to the corres- ponding state transformation (under a model
for the logic in question). For a state space
, and set of values
, let
be the set of states on
and
(including
), and for any formula
let
be the set of states which satisfies the formula. See [1] for details.
For initial state
we define
for every statement
, i.e. if the program is started in the non-terminating state then it cannot be guaranteed to terminate. (Starting the program in a non-terminating state simply means that some previous program in the sequence has failed to terminate, so this program can never actually start. This restriction simply means that a later statement in a sequence cannot somehow “recover” from non-termination of an earlier statement in the sequence the program).
The semantics for the recursive program is simply the intersection of the semantics for each finite truncation. The result is the least defined statement which is a refinement of all the truncations.
If the initial state space is empty, then there are two possible initial states:
and the single proper state
. For
the set of final states must be
, by definition. So the state transformation is entirely determined by its value on the initial state
. If the final state space is also empty, then there are exactly three distinct state transformations, corresponding to the three possible sets of states.1 The three state transformations are
,
and
where:
![]()
These correspond to the three fundamental statements
,
and
:
![]()
![]()
1Recall that if
is in the set of final states, then every other state has to be included: so
is not a valid final set of states.
Note that there are three different semantic function which use no variables, but only two semantically-dif- ferent formulae with no free variables (namely
and
). Under any interpretation of the logic, any formula with no free variables must be interpreted as either universally true or universally false. There is no way to map three different semantics onto two formulae: so this proves that a single formula is insufficient to re- present the semantics of a program.
3. The Abort and Behaviour Predicates
Since it is not possible to represent the semantics of a program using one formula, we will now consider how we can represent the denotational semantics of a program using two formulae from infinitary first order logic. The formulae are defining in terms of the weakest precondition.
For any program
and postcondition (condition on the final state space)
, the weakest precondition
is the weakest condition on the initial state space such that if the initial state satisfies
then
is guaranteed to terminate in a state which satisfies
.
In [1] , we show that
can be defined as a formula in infinitary logic and that refinement can be characterised by the weakest precondition as follows: for any to programs
and
with the same initial and final state spaces,
is a refinement of
, written
, if and only if for all postconditions
:
![]()
In the same paper, we also prove that it is not necessary to determine the weakest preconditions for all postconditions: two very simple postconditions are sufficient. These are the conditions
and
where
is a list of all the variables in
and
is a list of new variables, not appearing in either program, which are the doubly-primed versions of the variables in
. Then
if and only if:
![]()
For any statement
, the formula
describes precisely those initial states on which
is guaranteed to terminate. For each of these states, the formula
describes the behaviour of
in the sense that, if
is an initial state for which
terminates, and
is an extension of
which adds the variables
to the state with a given set of values, then
satisfies
precisely when the values assigned to
form a possible final state for
when they are assigned to the corresponding un- primed variables.
To be more precise, we will prove the following theorem:
Theorem 3.1. If
is the interpretation of
, then for every initial state
and final state
, the corresponding extended initial state
is in
, and conversely, every state in
is of the form
for some initial state
and
.
Proof: Suppose
is the interpretation of
as a state transformation from
to
, and let
be any initial state. Let
be any proper state in
(i.e. any element of
apart from
). Let
be the extension of
which adds
to the initial and final state spaces and preserves the values of these variables. Then
is the interpretation of
as a state transformation from
to
and for every varia- ble
, the initial and final values of
on
are identical. Let
be the state
extended to state space
which gives the variables in
the same values that the corresponding unprimed variables have in
. So, for every
,
, and
for
. Let
be the correspond- ing extension to
. Then, by the definition of
,
.
Claim:
is in the interpretation of
. To prove the claim, assume for contradiction that
is in
. Then
is guaranteed to terminate in a state which satisfies
, in other words, every state in
satisfies
. But state
is in
and within
, for each
,
. So
does not satisfy
, which is a contradiction.
Conversely, any state which satisfies
is of the form
for some
and
, since
cannot change the value of any variable in
. So, let
be any initial state which satisfies
, where
is the restriction of
to
and
is the restriction of
to
and where
is the state on
which corresponds to
. We claim that
. Assume for contradiction that
, then
is guaranteed to terminate on
(since otherwise
contains every state) and
is not a possible final state for
. So every final state in
differs from
. As before, let
be the extension of
over
such that
for all
. Then
for all
, and by definition of
, every final state in
differs from
. So,
terminates on
and every final state in
satisfies
. So
which is a contradiction.
As an example, for the program
If the final state space is
, then:
.
In [1] we also prove the Representation Theorem:
Theorem 3.2. For any statement
, let
. Then:
![]()
The representation theorem seems to imply that a third formula, namely
, is needed to fully characterise the behaviour of a program. However, this formula can be derived from the behaviour formula:
Theorem 3.3. For any statement
,
.
We define two formulae:
which captures the termination properties of
(the abort states) and
which captures the behaviour of
:
![]()
is true on precisely those initial states for which
can abort (not terminate), while
is true on initial states for which the values of
are the values of
in one of the possible final states. Note that an initial state for which
could abort will include all possible values in the set of final states, so we would ex- pect that
for all statements
.
If
is guaranteed to terminate and satisfy
and if
, then
is also guaranteed to terminate and satisfy
. So the weakest precondition is monotonic in the postcondition, and, since
, we have
, and therefore:
![]()
With these definitions we can prove that
and
fully characterise the refinement property:
Theorem 3.4. For any statements
and
, with the same initial and final state spaces,
is a refine- ment of
, written
, if and only if:
![]()
Note that the implications are in the opposite direction to the weakest precondition implications since
and
are both the negation of a weakest precondition.
With these definitions we can rewrite Theorem 3.2 as:
![]()
or, equivalently:
![]()
The three statements may be interpreted informally as stating:
1. If there is no defined behaviour (terminating or otherwise) then the statement is null;
2. Otherwise, if
is true, then the statement aborts;
3. Otherwise, new values
are assigned to the variables
such that
is satisfied.
For null-free programs,
, this is Dijkstra’s “Law of the Excluded Miracle” [2] , and so for these programs the initial guard is always equivalent to
, and
is true.
Theorem 3.5. Let
and
be any two formula, such that (1)
and (2) No variable in
ap- pears free in
. Let
![]()
Then
and
.
We have proved that:
1) Given any statement
, we can define the corresponding
and
by using weakest precondi- tions;
2) Given any two formulae,
and
, where
and no variable in
appears in
, we can de- fine a statement
such that
and
.
These results prove that the two formulae
and
completely capture the semantic behaviour of statement
.
Given any two formulae
and
we can define
as the formula
. Then
is true and none of the variables in
are free in
. So
and
satisfy the requirements for Theorem 3.5. Note that if
and
already satisfy the requirements, then
.
These comments motivate the definition of a function
which maps any two formulae
and
to a WSL statement:
![]()
By Theorem 3.5,
and
.
In the case where
and none of the variables in
appears free in
, we have:
and
.
Four fundamental programs are
,
,
and
for which the corresponding formulae are given in Table 1. From this table we see that:
![]()
when
is non-empty, then all three refinements are strict refinements. Note that
and
have the same behaviour but different termination conditions, while
and
have the same termination conditions but different behaviour. (When
is empty
is equivalent to
and the formula
is equivalent to
.)
Examples
Some example programs to illustrate the formulae:
![]()
![]()
![]()
![]()
Here,
is both more defined (terminating on more initial states) and more deterministic than
, and so
is a refinement of
. A refinement of a program can define any behaviour for initial states on which the original program aborts, so
is also a refinement of
. Finally,
is more deterministic than
in that it restricts the set of possible final states (for initial states with
the set of final states is empty).
These facts are reflected in the formulae in Table 2.
Clearly,
and
which shows that
. Also
and
which shows that
. However, it is not the case that
since when
in- itially,
must assign
the value 1, while
can non-deterministically choose to assign
the value 1 or 3. Conversely,
is not refined by
because
is defined on initial states for which
is not defined: namely, those initial states in which
.
Finally,
is a (strict) refinement of all the other programs, and none of the other programs is a refinement of
because
is null on initial states with
.
Given that
and
capture the semantics of a program, it should be possible to compute the formulae for a compound statement from the formulae for the components. For the primitive statements in the first level of WSL, the formulae are given in Table 3.
![]()
Table 1.
and
for some fundamental programs.
![]()
Table 2.
and
for the example programs.
![]()
Table 3.
and
for the atomic statements.
4. Computing A and B for Compound Statements
Given the two formulae
and
, which are in effect, the weakest preconditions on
for two par- ticular postconditions, we can determine the weakest precondition for any given postcondition. This means that we can compute
and
for any compound statement, given the corresponding formulae for the compo- nent statements.
For nondeterministic choice:
![]()
and similarly:
![]()
For deterministic choice:
![]()
and similarly:
![]()
For sequential composition:
![]()
In other words, for
to abort on an initial state,
must not be null and either
aborts or
ter- minates in a state in which
aborts.
To compute
we need to compute
, but this contains a postcondition which includes variables in
. We can solve this problem by computing the formula
and then renaming
to
in the result. Note that the postcondition
is simply
.
![]()
In other words, for
to be a possible final state for
on initial state
, either
aborts or there exists some intermediate state
which is a possible final state for
and for which
gives
as a possible final state when started in this initial state.
Recursion
is defined in terms of the set of all finite truncations. Define:
![]()
![]()
Then for any postcondition
:
![]()
So:
![]()
5. Temporal Logic
Temporal logic [3] is a class of logical theories for reasoning about propositions qualified in terms of time and can therefore be used to reason about finite and infinite sequences of states. These sequences can define an op- erational semantics for programs which maps each initial state to the set of possible histories: where a history is a possible sequence of states in the execution of a program. Since a formula can describe an infinite sequence of states: and therefore a non-terminating program, there would appear to be no need for the special state
to indicate non-termination, and therefore it would appear possible to represent the operational semantics of a pro- gram using a single formula in temporal logic.
This turns out not to be the case: a single formula is not sufficient, but two formulae (the temporal equivalent of the abort and behaviour predicates defined here) are sufficient. Lack of space precludes a full discussion of these questions in this paper.
NOTES
*Corresponding author.