Probabilistic Guarded Commands Mechanized in HOL

The probabilistic guarded-command language pGCL contains both demonic and probabilistic nondeterminism, which makes it suitable for reasoning about distributed random algorithms. Proofs are based on weakest precondition semantics, using an underlying logic of real- (rather than Boolean-) valued functions. We present a mechanization of the quantitative logic for pGCL using the HOL theorem prover, including a proof that all pGCL commands satisfy the new condition sublinearity, the quantitative generalization of conjunctivity for standard GCL. The mechanized theory also supports the creation of an automatic proof tool which takes as input an annotated pGCL program and its partial correctness specification, and derives from that a sufficient set of verification conditions. This is employed to verify the partial correctness of the probabilistic voting stage in Rabin's mutual-exclusion algorithm.