Hoare's logic for nondeterministic regular programs: A nonstandard approach

AbstractThis paper studies Hoare's logic for nondeterministic regular programs (with unbounded nondeterminism) from the point of view of nonstandard dynamic logic. We define a so-called continuous semantics which allows certain “infinitely long computations” and compare it with usual semantics, proving among other things the equivalence of both over “reasonable data types”. We also establish a completeness theorem for Hoare's calculus relative to continuous semantics, thereby generalizing a previous result of Csirmaz. The proof makes use of a normal form for regular programs which is perhaps interesting in its own right