In previous presentations a notion of probabilistic predicate and a Hoare style logic have been introduced. A basic probabilistic predicate gives the probability of a certain property. The predicates can be combined with both logical operators and arithmetical operators.

In this presentation a language with both nondeterminism and probability is considered. The result of executing a program in this language will be a state with both nondeterminism and probability. The probabilistic predicates can also be used to specify properties of these nondeterministic probabilistic states.

The Hoare style logic for reasoning about probabilistic programs is extended by adding a rule to deal with nondeterministic programs. The added rule is the same as the rule for nondeterminism known from Hoare logic.

An example illustrates the use of the logic and also shows how the logic can be used to check the results of a given probabilistic strategy for one player in a two player game.