As a starting point have a look at http://en.wikipedia.org/wiki/Predicate_transformer_semantics.