Partial correctness for probabilistic demonic programs

A. K. McIver*, Carroll Morgan

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

33 Citations (Scopus)


Recent work in sequential program semantics has produced both an operational (He et al., Sci. Comput. Programming 28(2, 3) (1997) 171-192) and an axiomatic (Morgan et al., ACM Trans. Programming Languages Systems 18(3) (1996) 325-353; Seidel et al., Tech Report PRG-TR-6-96, Programming Research group, February 1996) treatment of total correctness for probabilistic demonic programs, extending Kozen's original work (J. Comput. System Sci. 22 (1981) 328-350; Kozen, Proc. 15th ACM Symp. on Theory of Computing, ACM, New York, 1983) by adding demonic nondeterminism. For practical applications (e.g. combining loop invariants with termination constraints) it is important to retain the traditional distinction between partial and total correctness. Jones (Monograph ECS-LFCS-90-105, Ph.D. Thesis, Edinburgh University, Edinburgh, UK, 1990) defines probabilistic partial correctness for probabilistic, but again not demonic programs. In this paper we combine all the above, giving an operational and axiomatic framework for both partial and total correctness of probabilistic and demonic sequential programs; among other things, that provides the theory to support our earlier - and practical - publication on probabilistic demonic loops (Morgan, in: Jifeng et al. (Eds.), Proc. BCS-FACS Seventh Refinement Workshop, Workshops in Computing, Springer, Berlin, 1996).

Original languageEnglish
Pages (from-to)513-541
Number of pages29
JournalTheoretical Computer Science
Issue number1-2
Publication statusPublished - 6 Sep 2001
Externally publishedYes


  • Partial correctness
  • Probability
  • Program logic
  • Verification

Fingerprint Dive into the research topics of 'Partial correctness for probabilistic demonic programs'. Together they form a unique fingerprint.

Cite this