Program transformation rules describe the conditions under which it is possible to transform one program into another one which preserves the behaviour of the ﬁrst. They may be used to reason about such things as compiler optimisations, distributed algorithms or data reﬁnement. Such program transformations have traditionally been used to reason about standard (i.e., non-probabilistic) programs which may possibly include a nondeterministic choice operator. In this thesis we aim to identify and verify transformation theorems for probabilistic programs. In particular we examine probabilistic programs which may contain a discrete proba¬bilistic choice operator in addition to one or two nondeterministic choice operators. Such probabilistic programs may be used for reasoning about distributed proba¬bilistic algorithms, reliable systems modelling, or probabilistic games.
The probabilistic transformation theorems are investigated and veriﬁed using an algebraic approach since this method has been successfully applied to this task for standard programs. We only consider probabilistic program models in which choices are resolved – intuitively speaking – according to the execution order of the program. Such probabilistic program models, even those which only include one form of nondeterministic choice, do not satisfy all of the algebraic properties of standard programs which may only include one form of choice. This means that many well known program transformation theorems do not hold for these programs.
We algebraically investigate transformation theorems for a non-reactive proba¬bilistic program model in detail. This model, an expectation-transformer model, is suitable for reasoning about total program correctness, and can be used to express guards, assertions, recursively deﬁned statements, in addition to probabilistic, de¬monic and angelic choice. As part of this work, transformation theorems for weak and strong iteration statements, as well as non-reactive probabilistic action systems and while loops are developed.
Abstract algebras that are suitable for expressing and verifying many of the transformation theorems we had investigated in the total-correctness model are then identiﬁed, discussed, and used to specify commonalities between diﬀerent pro¬gram models. In particular we use the algebras to show that standard programs which may include two forms of choice share many algebraic similarities with the probabilistic programs we have considered, and that most of our transformation theorems are equally valid for these kinds of programs. We also develop a sim¬ple reactive program language which is capable of modelling reactive probabilistic action systems, and we show that this model also satisﬁes many of the same alge¬braic properties as the non-reactive model. This work demonstrates how it may be possible to reason about transformations of reactive probabilistic programs in the same way it is possible to reason about non-reactive ones.