Soundness of a purely syntactical formalization of weakest preconditions
Rudolf Berghammer · Electronic Notes in Theoretical Computer Science · 2000
We present a purely syntactical definition of E.W. Dijkstra's predicate transformer wp for nondeterministic while-programs in infinitary logic. Then we show that it is sound with respect to a definition of weakest preconditions given in terms of denotational semantics.