Skip to main content
SpringerLink
Log in

Is “some-other-time” sometimes better than “sometime” for proving partial correctness of programs?

  • Published:
Studia Logica Aims and scope Submit manuscript

Abstract

The main result of this paper belongs to the field of the comparative study of program verification methods as well as to the field called nonstandard logics of programs. We compare the program verifying powers of various well-known temporal logics of programs, one of which is the Intermittent Assertions Method, denoted as Bur. Bur is based on one of the simplest modal logics called S5 or “sometime”-logic. We will see that the minor change in this “background” modal logic increases the program verifying power of Bur. The change can be described either technically as replacing the “reflexive version” of S5 with an “irreflexive version”, or intuitively as using the modality “some-other-time” instead of “sometime”. Some insights into the nature of computational induction and its variants are also obtained.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. M. Abadi, The power of temporal proofs, Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science, Ithaca, NY, June 1987, pp. 123–130.

  2. A. Amir, Expressive completeness failure in branching time structures, Journal of Computer and System Sciences 34, 1987, pp. 27–42.

    Google Scholar 

  3. H. Andréka, Sharpening the characterization of the power of Floyd's method, in: Logic of Programs and their Applications, ed., A. Salwicki (Proc. Conf. Poznań 1980, Lecture Notes in Computer Science 148, Springer-Verlag 983, pp. 1–26.

  4. H. Andréka, K. Balogh, K. Lábadi, I. Németi and P. Tóth, Plan for improving a working program verifier program, Software Dept. of Computing Center of the Heavy Industries, Preprint 1974, Budapest (in Hungarian).

  5. H. Andréka, I. Németi and I. Sain, A complete logic for reasoning about programs via nonstandard model theory, Parts I–II, Theoretical Computer Science 17 (1982), pp. 193–212 and pp. 259–278.

    Google Scholar 

  6. R. M. Burstall, Program proving as hand simulation with a little induction, IFIP Congress, Stockholm, August 3–10, 1974.

  7. L. Csirmaz, On the completeness of proving partial correctness, Acta Cybernetica, Tom 5, Fasc 2, Szeged, 1981, pp. 181–190.

    Google Scholar 

  8. L. Csirmaz, Programs and program verifications in a general setting, Theoretical Computer Science 16 (1981), pp. 199–210.

    Google Scholar 

  9. R. Goldblatt, Axiomatizing the Logic of Computer Programming, Lecture Notes in Computer Science 130, Springer-Verlag, 1982.

  10. M. T. H. Gonzàlez and M. R. Artalejo, Hoare's logic for nondeterministic regular programs: A nonstandard approach, Preprint Universidad de Madrid 84/85/cc-1, 1985. Abstracted in 12th International Colloquium on Automata, Languages and Programming, Greece, 1985.

  11. P. Hájek, Some conservativeness results for nonstandard dynamic logic, in: Algebra, Combinatorics and Logic in Computer Science, ed., J. Demetrovics, G. Katona, A. Salomaa (Proc. Conf. Györ Hungary 1983) Colloq. Math. Soc. J. Bolyai Vol 42, North-Holland, 1986, pp. 443–449.

  12. L. Henkin, Completeness in the theory of types, Journal of Symbolic Logic 15, 1950, pp. 81–91.

    Google Scholar 

  13. L. Henkin, J. D. Monk and A. Tarski, Cylindric Algebras Part II, North-Holland, 1985.

  14. M. Immerman and D. Kozen, Definability with bounded number of bound variables, Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science, Ithaca, NY, June 1987, pp. 236–244.

  15. J. A. Makowsky and I. Sain, On the equivalence of weak second order and nonstandard time semantics for various program verification systems. Proceedings of the First Annual IEEE Symposium on Logic in Computer Science, Cambridge, MA (USA), June 1986, pp. 293–300.

  16. J. A. Makowsky and I. Sain, Weak second order characterizations of various program verification systems, Technical Report # 457, Technion — Israel Institute of Technology, Comp. Sci. Dept., June 1987. Submitted to Theoretical Computer Science.

  17. Z. Manna and A. Pnueli, The modal logic of programs, in: International Colloquium on Automata, Languages and Programming '79, Graz, Lecture Notes in Computer Science 71, Springer-Verlag, 1979, pp. 385–409.

  18. I. Németi, Nonstandard dynamic logic, in: Logics of Programs, ed., D. Kozen, (Proc. Conf. New York 1981) Lecture Notes in Computer Science 131, Springer-Verlag, 1982, pp. 311 348.

  19. A. Pasztor, Recursive programs and denotational semantics in absolute or nonstandard logics of programs, Preprint of Florida International University Comp. Sci. Dept., 1987.

  20. A. Pnueli, The temporal semantics of concurrent programs, Theoretical Computer Science 13 (1981), pp. 45–60.

    Google Scholar 

  21. A. Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science, 1977, pp. 46–57. Revised version: Preprint of the Weizman Institute of Science, May 1981.

  22. I. Sain, Successor axioms for time increase the program verifying power of full computational induction, Preprint No 23/1983. Math. Inst. Hungar. Acad. Sci., 1983.

  23. I. Sain, Structured nonstandard dynamic logic, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik Heft 3, Band 30, 1984, pp. 481 497.

    Google Scholar 

  24. I. Sain, A simple proof for completeness of Floyd method, Theoretical Computer Science 35 (1985). pp. 345 348.

    Google Scholar 

  25. I. Sain, Relative program verifying powers of the various temporal logics, Preprint of the Mathematical Institute of Hungarian Academy of Sciences, No. 40 (1985). An extended abstract of this is [26].

  26. I. Sain, The reasoning powers of Burstall's (modal logic) and Pnueli's (temporal logic) program verification methods, in: Logics of Programs, ed., R. Parikh (Proc. Conf. Brooklyn USA 1985) Lecture Notes in Computer Science 193, Springer-Verlag, pp. 302–319.

  27. I. Sain, Dynamic logic with nonstandard model theory, Dissertation, Hungarian Academy of Sciences, Budapest, 1986 (in Hungarian).

    Google Scholar 

  28. I. Sain, Total correctness in nonstandard logics of programs, Theoretical Computer Science 50 (1987), to appear. An extended abstract of this appeared in Bulletin of the Section of Logic Vol. 12, No. 2, Warsaw-Łódź 1983, pp. 64–70.

Download references

Author information

Authors and Affiliations

  1. Mathematical Institute of The Hungarian Academy of Sciences, PF 127, Budapest 1364, Hungary

    Ildikó Sain

Authors
  1. Ildikó Sain
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

This project was supported by the Hungarian National Foundation for Scientific Research, Grant No. 1810.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Sain, I. Is “some-other-time” sometimes better than “sometime” for proving partial correctness of programs?. Stud Logica 47, 279–301 (1988). https://doi.org/10.1007/BF00370557

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF00370557

Keywords

Search

Navigation