Logic of Programs 1983: Logics of Programs pp 206-220 | Cite as

Reasoning about procedures as parameters

  • S. M. German
  • E. M. ClarkeJr.
  • J. Y. Halpern
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 164)


Ordinary Variable Axiom System Procedure Call Axiom Scheme High Order Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    de Bakker, J. W., Klop, J. W., Meyer, J.-J. Ch. Correctness of programs with function procedures. Tech. Rept. IW 170/81, Mathematisch Centrum, Amsterdam, 1981.Google Scholar
  2. 2.
    Clarke, H. M. "Programming language constructs for which it is impossible to obtain good Hoare-like axioms." jACM 26 (1979), 129–147.Google Scholar
  3. 3.
    Clarke, E. M., Jr., German, S., and Halpern, J. Y. "Effective axiomatization of Hoare logics." JACM 30 (1983), 612–636.Google Scholar
  4. 4.
    Cook, S. A. "Soundness and completeness of an axiom system for program verification." SIAM J. Comput. 7 (1978), 70–90.Google Scholar
  5. 5.
    Damm, W. and Josko, B. A sound and relatively complete Hoare-logic for a language with higher type procedures. Tech. Rept. Bericht No. 77, Lehrstuhl fur Informatik II, RWTH Aachen, April, 1982.Google Scholar
  6. 6.
    Damm, W. and Josko, B. personal communication.Google Scholar
  7. 7.
    German, S. Relative completeness proofs for languages with infinite range.Google Scholar
  8. 8.
    German, S. and Halpern, J. On the power of acceptable programming languages with recursion.Google Scholar
  9. 9.
    Olderog, E.-R. "Sound and complete Hoare-like calculi based on copy rules." Acta Informatica 16 (1981), 161–197.Google Scholar
  10. 10.
    Olderog, E.-R. "Hoare-style proof and formal computations." Jahrestagugn, IFB 50 GI-II (1981), 65–71.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • S. M. German
    • 1
  • E. M. ClarkeJr.
    • 2
  • J. Y. Halpern
    • 3
  1. 1.Harvard UniversityUSA
  2. 2.Carnegie-Mellon UniversityUSA
  3. 3.IBM ResearchSan Jose

Personalised recommendations