  We study transformational program logics for correctness and incorrectness
that we extend to explicitly handle both termination and nontermination. We
show that the logics are abstract interpretations of the right image
transformer for a natural relational semantics covering both finite and
infinite executions. This understanding of logics as abstractions of a
semantics facilitates their comparisons through their respective abstractions
of the semantics (rather that the much more difficult comparison through their
formal proof systems). More importantly, the formalization provides a
calculational method for constructively designing the sound and complete formal
proof system by abstraction of the semantics. As an example, we extend Hoare
logic to cover all possible behaviors of nondeterministic programs and design a
new precondition (in)correctness logic.
