Completeness of Hoare Logic over Nonstandard Models

The nonstandard approach to program semantics has successfully resolved the completeness problem of Floyd-Hoare logic. The kno