Models of program logics

We briefly survey the major proposals for models of programs and show that they all lead to the same propositional theory of programs. Methods of algebraic logic dominate in the proofs. One of the connections made between the models, that involving language models, is quite counterintuitive. The common theory has already been shown to be complete in deterministic exponential time; we give here a simpler proof of the upper bound.