VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
- 1 June 2002
- journal article
- Published by World Scientific Pub Co Pte Ltd in International Journal of Foundations of Computer Science
- Vol. 13 (3) , 315-340
- https://doi.org/10.1142/s012905410200114x
Abstract
Probability, be it inherent or explicitly introduced, has become an important issue in the verification of programs. In this paper we study a formalism which allows reasoning about programs which can act probabilistically. To describe probabilistic programs, a basic programming language with an operator for probabilistic choice is introduced and a denotational semantics is given for this language. To specify propertics of probabilistic programs, standard first order logic predicates are insufficient, so a notion of probabilistic predicates is introduced. A Hoare-style proof system to check properties of probabilistic programs is given. The proof system for a sublanguage is shown to be sound and complete; the properties that can be derived are exactly the valid properties. Finally some typical examples illustrate the use of the probabilistic predicates and the proof system.Keywords
This publication has 7 references indexed in Scilit:
- Probabilistic predicate transformersACM Transactions on Programming Languages and Systems, 1996
- Reactive, Generative, and Stratified Models of Probabilistic ProcessesInformation and Computation, 1995
- Probabilistic VerificationInformation and Computation, 1993
- Bisimulation through probabilistic testingInformation and Computation, 1991
- A probabilistic PDLJournal of Computer and System Sciences, 1985
- Soundness and Completeness of an Axiom System for Program VerificationSIAM Journal on Computing, 1978
- An axiomatic basis for computer programmingCommunications of the ACM, 1969