Weakly expressive models for Hoare logic (Q805248): Difference between revisions

The author generalizes the notion of complete models for Hoare logic to the weakly expressive models. After some preliminaries about Hoare logic, the author introduces the weakly expressive models and proves some important features of them. The main results are that the complete models are weakly expressive and that a model is expressive if the domain of every program is definable.