Correctness of programs over poor signatures
A poor signature consists of one (unary) function symbol, a symbol for equality and a number of constant symbols. Due to the lack of internal structure, interpretations of poor signatures differ from interpretations of richer signatures in some respects. One of them is the completeness of Hoare-like systems relative to the first-order theory of the interpretation.
We demonstrate that Hoare-like proof systems for partial correctness are incomplete in any infinite (and not uniformly locally finite) interpretation of a poor signature, even if the systems are supplied with the first-order theory of the interpretation. The reason is that there are always relations which are definable by while-programs but not by formulas. This is shown by an application of a result used in model theory. We also answer the question which enrichments of the signature are necessary and sufficient to allow (nontrivial) infinite interpretations where Hoare-like systems are complete.
KeywordsFunction Symbol Proof System Boolean Formula Relation Symbol Constant Symbol
Unable to display preview. Download preview PDF.
- [BT2]Bergstra, J. A. and Tucker, J. V. Hoare 's logic for programming languages with two data types. TCS 24 (1984) 215–221.Google Scholar
- [F]Friedman, H. Generalized Turing algorithms, and elementary recursion theory. in: Gandy and Yates (eds) Logic Colloquium '69, North-Holland, Amsterdam (1971) 361–390.Google Scholar
- [G]Gaifman, H. Finiteness is not a Σ 0-property. Isr. J. Math. 19 (1974) 359–368.Google Scholar
- [GeHa]German, S. M. and Halpern, J. Y. On the power of the hypothesis of expressiveness. IBM Res. Rep. RJ 4079 (45457) Yorktown Heights (1983).Google Scholar
- [GrHu]Grabowski, M. and Hungar, H. On the existence of effective Hoare logics. 3rd LiCS (1988) 428–435.Google Scholar
- [H]Harel, D. First-order dynamic logic. Springer LNCS 68 New York (1979).Google Scholar
- [Li]Lipton, R. J. A necessary and sufficient condition for the existence of Hoare logics. 18th FoCS (1977) 1–6.Google Scholar
- [LS]Loeckx, J. and Sieber, K. The foundation of program verification. 2nd ed., Wiley-Teubner (1987).Google Scholar
- [M]Marcus, L. Minimal models of theories of one function symbol. Isr. J. Math. 18 (1974) 117–131.Google Scholar