Overview of results

For Dijkstra's language a model has been provided which extends predicate transformers (which map postconditions to weakest preconditions) to expectation transformers, mapping expected yields over final states to most-pessimistic expected payoffs over initial states. A relational model of the language has also been considered and the healthy subset, of transformers corresponding to relational code, has been characterised using a simple sublinearity property.

A programmer is able to use a formal method only if it provides laws enabling him to verify design decisions against specifications. Sound proof rules for the language have been provided and shown to deal with the combination of probabilistic choice and nondeterminism. For the important topic of loop termination it has been shown, for example, that a loop terminates if on each iteration its body offers merely a nonzero probability of decreasing some variant. In program developments which change the state space, simulations in the standard theory are replaced by transformers recording conditional probabilistic information between abstract and concrete states. It is unknown, for probabilistic systems, whether a single probabilistic simulation rule is complete for verifying development steps.

Probability and nondeterminism are each subtle enough that it might be feared formal complete reasoning about their combination would be impractical. The probabilistic formal method has thus been demonstrated on a variety of realistic examples including: probabilistic algorithms of Rabin have been expressed and verified; the system of probabilistic dining philosophers has been studied and its symmetric solution verified simply using a probabilistic variant; probabilistic communications protocols have been described; the solution to the popular Monty Hall puzzle has been verified; and the steam-boiler example from critical-systems theory has been analysed probabilistically.

Proof of correctness of probabilistic loops is facilitated by the study of a temporal logic in which probabilistic claims are considered over loop iterations. Such a logic applies not just to loops in a sequential language but also to reactive systems. A probabilistic temporal logic has been produced which strengthens previous logics by expressing explicit probabilities.

The semantic models for probability are of course more expressive than standard models. A simplification of one of them is strong enough to provide a single formalism able to express the two forms of predicate transformer correctness: wp and wlp. Another is able to quantify the flow of information between procedures; that model and its laws promise much for the treatment of security.

Process algebra provides an important alternative formal method, based on synchronisation of processes evolving in parallel. The failures/divergences model of the process algebra CSP has been extended to incorporate probabilistic combinator in such a way that its refinement relation now expresses the probability with which one probabilistic process refines another. Standard features of CSP are preserved by the probabilistic construction though some new -- and characteristic -- laws arise so that care is required in replaying standard reasonining. In standard CSP a hierarchy of models is provided for reasoning at progressively finer levels of observation; it too has been extended to the probabilistic setting.

Next: The formal method Up: Contents Page Previous: The Context