Adequacy for Predicate Transformer Semantics
This paper establishes a generic framework to prove adequacy for predicate transformer semantics with respect to an appropriately designed operational semantics, and covers a wide range of instances, including total expected costs, cost moments, conditional expectations, and expected multiplicative rewards of probabili...