
This paper defines a formal logic PrDL whose syntax derives from Pratt's first-order dynamic logic and whose semantics is an extension of Kozen's for probabilistic programs. An axiom system for PrDL is given and shown to be complete relative to an extension of first-order analysis. For discrete probabilities it is shown that first-order analysis actually suffices. Some precursors of this paper are \textit{J. H. Reif's} propositional version [12th ACM Symp. Theory of Computing, 8-13 (1980)] and \textit{L. Ramshaw's} semiformal system based on the Floyd-Hoare inductive assertion method [Ph. D. thesis (1981), Stanford University].
Specification and verification (program logics, model checking, etc.), Computer Networks and Communications, Applied Mathematics, Probability and inductive logic, Theoretical Computer Science, dynamic logic, Computational Theory and Mathematics, completeness, probabilistic programs, semantics, Abstract data types; algebraic specification
Specification and verification (program logics, model checking, etc.), Computer Networks and Communications, Applied Mathematics, Probability and inductive logic, Theoretical Computer Science, dynamic logic, Computational Theory and Mathematics, completeness, probabilistic programs, semantics, Abstract data types; algebraic specification
| citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 53 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 1% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
