Completeness of Hoare logic relative to the standard model. (English) Zbl 1444.03122
Steffen, Bernhard (ed.) et al., SOFSEM 2017: theory and practice of computer science. 43rd international conference on current trends in theory and practice of computer science, Limerick, Ireland, January 16–20, 2017, Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10139, 119-131 (2017).
Summary: The general completeness problem of Hoare logic relative to the standard model \(N\) of Peano arithmetic has been studied by Cook, and it allows for the use of arbitrary arithmetical formulas as assertions. In practice, the assertions would be simple arithmetical formulas, e.g. of a low level in the arithmetical hierarchy. This paper further studies the completeness of Hoare logic relative to \(N\) with assertions restricted to subclasses of arithmetical formulas. Our completeness results refine Cook’s result by reducing the complexity of the assertion theory.
For the entire collection see [Zbl 1355.68020].
For the entire collection see [Zbl 1355.68020].
MSC:
| 03B70 | Logic in computer science |
| 03C62 | Models of arithmetic and set theory |
| 03F30 | First-order arithmetic and fragments |
Keywords:
Hoare logic; Peano arithmetic; arithmetical hierarchy; standard model; relative completenessReferences:
| [1] | Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576–580 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259 |
| [2] | Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, 70–90 (1978) · Zbl 0374.68009 · doi:10.1137/0207005 |
| [3] | Mirkowska, G., Salwicki, A.: Algorithmic Logic. Springer, Dordrecht (1987) · Zbl 0648.03018 |
| [4] | Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000) · Zbl 0976.68108 |
| [5] | Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55–74 (2002) |
| [6] | Apt, K.R.: Ten years of Hoare’s logic: a survey - Part I. ACM Trans. Program. Lang. Syst. 3(4), 431–483 (1981) · Zbl 0471.68006 · doi:10.1145/357146.357150 |
| [7] | Apt, K.R.: Ten years of Hoare’s logic: a survey - Part II: nondeterminism. Theoret. Comput. Sci. 28, 83–109 (1984) · Zbl 0523.68015 · doi:10.1016/0304-3975(83)90066-X |
| [8] | Kleymann, T.: Hoare logic and auxiliary variables. Formal Aspects Comput. 11, 541–566 (1999) · Zbl 0978.03026 · doi:10.1007/s001650050057 |
| [9] | Nipkow, T.: Hoare logics in Isabelle, HOL. In: Proof and System-Reliability, pp. 341–367, Kluwer Academic Publishers (2002) · Zbl 1097.68632 · doi:10.1007/978-94-010-0413-8_11 |
| [10] | Kaye, R.: Models of Peano Arithmetic. Oxford University Press, New York (1991) · Zbl 0744.03037 |
| [11] | Bergstra, J.A., Tucker, J.V.: Hoare’s logic and Peano’s arithmetic. Theoret. Comput. Sci. 22, 265–284 (1983) · Zbl 0497.68007 · doi:10.1016/0304-3975(83)90107-X |
| [12] | Boolos, G.S., Burgess, J.P., Jeffrey, R.C.: Computability and Logic, 5th edn. Cambridge University Press, Cambridge (2007) · Zbl 1154.03001 · doi:10.1017/CBO9780511804076 |
| [13] | Soare, R.I.: Recursively Enumerable Sets and Degrees. Springer, Heidelberg (1987) · Zbl 0667.03030 · doi:10.1007/978-3-662-02460-7 |
| [14] | Apt, K., Bergstra, J.A., Meertens, L.G.L.T.: Recursive assertions are not enough-or are they? Theoret. Comput. Sci. 8, 73–87 (1979) · Zbl 0393.68016 · doi:10.1016/0304-3975(79)90058-6 |
| [15] | Clarke, E.M.: Programming language constructs for which it is impossible to obtain good Hoare axiom systems. J. ACM 26, 129–147 (1979) · Zbl 0388.68008 · doi:10.1145/322108.322121 |
| [16] | Lipton, R.J.: A necessary and sufficient condition for the existence of Hoare logics. In: IEEE Symposium on Foundations of Computer Science, pp. 1–6 (1977) · doi:10.1109/SFCS.1977.1 |
| [17] | Clarke, E.M., German, S.M., Halpern, J.Y.: Effective axiomatizations of Hoare logics. J. ACM 30, 612–636 (1983) · Zbl 0627.68010 · doi:10.1145/2402.322394 |
| [18] | Grabowski, M.: On relative completeness of Hoare logics. Inf. Control 66, 29–44 (1985) · Zbl 0586.68027 · doi:10.1016/S0019-9958(85)80010-3 |
| [19] | Bergstra, J.A., Tucker, J.V.: Expressiveness and the completeness of Hoare’s logic. J. Comput. Syst. Sci. 25, 267–284 (1982) · Zbl 0549.68021 · doi:10.1016/0022-0000(82)90013-7 |
| [20] | Xu, Z., Sui, Y., Zhang, W.: Completeness of Hoare logic with inputs over the standard model. Theoret. Comput. Sci. 612, 23–28 (2016) · Zbl 1333.68182 · doi:10.1016/j.tcs.2015.08.004 |
| [21] | Kozen, D., Tiuryn, J.: On the completeness of propositional Hoare logic. Inf. Sci. 139, 187–195 (2001) · Zbl 0996.03022 · doi:10.1016/S0020-0255(01)00164-5 |
| [22] | Davis, M.: Computability & Unsovability. Courier Dover Publications, New York (1982) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
