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