# Correctness of programs over poor signatures

## Abstract

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.

## Keywords

Function Symbol Proof System Boolean Formula Relation Symbol Constant Symbol## Preview

Unable to display preview. Download preview PDF.

## References

- [A]Apt, K.R.
*Ten years of Hoare's logic: A survey—part I*. ACM TOPLAS**3**(1981) 431–483.CrossRefGoogle Scholar - [BT1]Bergstra, J. A. and Tucker, J. V.
*Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs*. TCS**17**(1982) 303–315.CrossRefGoogle Scholar - [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 - [CGH]Clarke, E. M., German, S. M. and Halpern, J. Y.
*Effective axiomatizations of Hoare logics*. JACM**30**(1983) 612–636.CrossRefGoogle Scholar - [Co]Cook, S. A.
*Soundness and completeness of an axiom system for program verification*. SIAM J. Comp.**7**(1978) 70–90.CrossRefGoogle 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]
- [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 - [HP]Harel, D. and Peleg, D.
*On static logics, dynamic logics, and complexity classes*. Inf. and Contr.**60**(1984) 86–102.CrossRefGoogle Scholar - [KU]Kfoury, A. J. and Urzyczyn, P.
*Necessary and sufficient conditions for the universality of programming formalisms*. Acta Inf.**22**(1985) 347–377.CrossRefGoogle 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 - [0]Olderog, E.-R.
*On the notion of expressiveness and the rule of adaptation*. TCS**24**(1983) 337–347CrossRefGoogle Scholar - [TU]Tiuryn, J. and Urzyczyn, P.
*Some relationships between logics of programs and complexity theory*. TCS**60**(1988) 83–108.CrossRefGoogle Scholar - [U]Urzyczyn, P.
*A necessary and sufficient condition in order that a Herbrand interpretation is expressive with respect to recursive programs*. Inf. and Contr.**56**(1983) 212–219.CrossRefGoogle Scholar - [W]Wand, M.
*A new incompleteness result for Hoare's system*. JACM**25**(1978) 168–175.CrossRefGoogle Scholar