Skip to main content

On expressive interpretations of a Hoare-logic for Clarke's language L4

  • Contibuted Papers
  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 166))

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. de Bakker, J.W./Klop, J.W./Meyer, J.-J.Ch.: Correctness of programs with function procedures. Report IW 170/81, Mathematisch Centrum, Amsterdam (1981)

    Google Scholar 

  2. Clarke, E.M.: Programming language constructs for which it is impossible to obtain good Hoare-like axioms. JACM 26, 129–147 (1979)

    Google Scholar 

  3. Clarke, E.M./German, S.M./Halpern, J.Y.: On effective axiomatizations of Hoare-logics. 9th Annual ACM Symp. on Principles of Programming Languages, 309–321 (1982)

    Google Scholar 

  4. Constable, R./Egli, H.: Computability concepts for programming language semantics. TCS 2, 133–145 (1976)

    Google Scholar 

  5. Damm, W./Josko, B.: A sound and relatively* complete Hoare logic for a language with higher type procedures. Acta Informatica 20, 59–101 (1983)

    Google Scholar 

  6. German, S.M./Clarke, E.M./Halpern, J.Y.: A stronger axiom system for reasoning about procedures as parameters. Workshop on Logics of Programs, Pittsburgh (1983)

    Google Scholar 

  7. Hoare, C.A.R.: An axiomatic basis for computer programming. CACM 12, 576–583 (1969)

    Google Scholar 

  8. Josko, B.: On expressive interpretations of a Hoare-logic for a language with higher type procedures. Schriften z. Inf. u. Angewandt. Math. Nr. 88, Aachen (1983)

    Google Scholar 

  9. Josko, B.: A Hoare-calculus for ALGOL-like programs with finite mode procedures without global variables. (in preparation)

    Google Scholar 

  10. Josko, B.: A note on expressivity definitions in Hoare-logics. Schriften z. Inf. u. Angewandt. Math. Nr. 80, TH Aachen (1982)

    Google Scholar 

  11. Kanda, A.: Effective solutions of recursive domain equations. Warwick (1979)

    Google Scholar 

  12. Langmaack, H.: On procedures as open subroutines I, II. Acta Informatica 2, 311–333 (1973) and 3, 227–241 (1974)

    Google Scholar 

  13. Langmaack, H.: Aspects of programs with finite modes. Proc. of the Int. Conf. on Foundations of Computation Theory (1983)

    Google Scholar 

  14. Langmaack, H./Olderog, E.-R.: Present-day Hoare-like systems for programming languages with procedures: power limits and most likely extensions. Proc. 7th Coll. Automata, Languages and Programming, LNCS 85, 363–373 (1980)

    Google Scholar 

  15. Lipton, R.J.: A necessary and sufficient condition for the existence of Hoarelogics. 18th IEEE Symp. on Foundations of Computer Science, 1–6 (1977)

    Google Scholar 

  16. Olderog, E.-R.: Sound and complete Hoare-like calculi based on copy rules. Acta Informatica 16, 161–197 (1981)

    Google Scholar 

  17. Olderog, E.-R.: Hoare-style proof and formal computations. 11. GI-Jahrestagung, IFB 50, 65–71 (1981)

    Google Scholar 

  18. Olderog, E.-R.: Correctness of programs with PASCAL-like procedures without global variables. (to appear in TCS)

    Google Scholar 

  19. Rogers, H.: Theory of recursive functions and effective comptability. McGraw-Hill

    Google Scholar 

  20. Trakhtenbrot, B.A./Meyer, A.E./Halpern, J.Y.: From denotational to operational and axiomatic semantics for ALGOL-like languages. Workshop on Logics of Programs, Pittsburgh (1983)

    Google Scholar 

  21. Takeuti, G.: Proof theory. North-Holland (1975)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

M. Fontet K. Mehlhorn

Rights and permissions

Reprints and permissions

Copyright information

© 1984 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Josko, B. (1984). On expressive interpretations of a Hoare-logic for Clarke's language L4 . In: Fontet, M., Mehlhorn, K. (eds) STACS 84. STACS 1984. Lecture Notes in Computer Science, vol 166. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-12920-0_7

Download citation

  • DOI: https://doi.org/10.1007/3-540-12920-0_7

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-12920-2

  • Online ISBN: 978-3-540-38805-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics