Non-deterministic expressions and predicate transformers. - Morris, Joseph M.
Keywords: Non-deterministic expression; Weakest preconditions; Refinement calculus