Proof Engineering With Predicate Transformer Semantics