Formalizing Dijkstra's predicate transformer wp in weak second-order logic

AbstractWe present a purely syntactical but nevertheless handy definition of Dijkstra's predicate transformer wp in weak second-order logic. This formalization allows us to prove a normal form theorem of wp, from which interesting properties can be inferred. In particular, it turns out that wp(P,·) is a homomorphism on the class of formulae in the formalism considered