The M-computations induced by accessibility relations in nonstandard models M of Hoare logic

Hoare logic 1] is a logic used as a way of specifying semantics of programming languages, which has been extended to be a separation logic to reason about mutable heap structure 2]. In a model M of Hoare logic, each program α induces an M-computable function f _α ^M on the universe of M; and the M-recursive functions are defined on M. It will be proved that the class of all the M-computable functions f _α ^M induced by programs is equal to the class of all the M-recursive functions. Moreover, each M-recursive function is \(\sum {_1^{{N^M}}} \)-definable in M, where the universal quantifier is a number quantifier ranging over the standard part of a nonstandard model M.