Predicate transformer semantics by Ernest G. Manes