Received 13 February 2014; revised 10 March 2014; accepted 18 March 2014

ABSTRACT

Can the semantics of a program be represented as a single formula? We show that one formula is insufficient to handle assertions, refinement or slicing, while two formulae are sufficient:, defining non-termination, and, defining behaviour. Any two formulae and will de- fine a corresponding program. Refinement is defined as implication between these formulae.

Keywords:

Formal Methods, Refinement, Non-Termination, Non-Determinism, Weakest Precondition, Temporal Logic, Wide-Spectrum Language

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.¹ The three state transformations are, and where:

These correspond to the three fundamental statements, and :

¹Recall 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.

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.

References

NOTES

^*Corresponding author.