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

Abstract

Hoare logic 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. 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 Σ^NM_{<?Pub Caret1?>1} -definable in M, where the universal quantifier is a number quantifier ranging over the standard part of a nonstandard model M.

Keywords

Hoare logic / recursive function / computable function / nonstandard model of Peano arithmetic

References

[1] Hoare C A R. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12(10), 576–583

[2] Apt K R. Ten years of Hoare’s logic: a survey-part 1. ACM Transactions on Programming Languages and Systems, 1981, 3(4), 431–483

[3] Bergstra J A, Tucker J V. Expressiveness and the completeness of Hoare’s logic. Journal of Computer and System Science, 1982, 25(3), 267–284

[4] Kozen D, Tiuryn J. On the completeness of propositional Hoare logic. Information Science, 2001, 139(3), 187–195

[5] Lamport L, Schneider F B. The “Hoare logic" of CSP, and all that. ACM Transactions on Programming Languages and Systems, 1984, 6(2), 281–296

[6] O’Hearn P W, Yang H, Reynolds J C. Separation and information hiding. In: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 2004, 268–280

[7] Parkinson M, Bierman G. Separation logic and abstraction. ACM SIGPLAN Notices, 2005, 40(1): 247–258

[8] Reynolds J C. Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. 2002, 55–74

[9] Cook S A. Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing, 1978, 7(1): 70–90

[10] Rogers H. Theory of Recursive Functions and Effective Computability. New York: McGraw-Hill, 1967

[11] Kaye R. Models of Peano Arithmetic. Oxford: Oxford University Press, 1991

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag Berlin Heidelberg