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