|
Abstract : |
The work is supported by the EPSRC. Abstract. Let predicate P be converted from Boolean to numeric type by writing hP i, with hfalsei being 0 and htruei being 1, so that in a degenerate sense hP i can be regarded as `the probability that P holds in the current state'. Then add explicit numbers and arithmetic operators, to give a richer language of arithmetic formulae into which predicates are embedded by h\Deltai. Abrial's generalised substitution language GSL can be applied to arithmetic rather than Boolean formulae with little extra effort. If we add a new operator p \Phi for probabilistic choice, it then becomes `pGSL': a smooth extension of GSL that includes random algorithms within its scope., |
