Skip to main content
SpringerLink
Log in

Semantical Analysis of Specification Logic, 2

  • Chapter
Algol-like Languages

Part of the book series: Progress in Theoretical Computer Science ((PTCS))

Abstract

The “specification logic” of J. C. Reynolds (1982) is a formal system for proving partial-correctness properties of programs in an Algol-like language with higher-order procedures. In a previous publication (Tennent, 1990), a model was presented that validates all axioms of the system except those involving non-interference formulas for procedural phrases. Following Reynolds, non-interference for procedural phrases was there defined syntactically, by induction on types.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • Barringer, H., Cheng, J. H., and Jones, C. B. (1984). A logic covering undefinedness in program proofs. Acta Informatica, 21: 251–269.

    Article  MathSciNet  MATH  Google Scholar 

  • Damm, W. and Josko, B. (1983). A sound and relatively*-complete Hoare-logic for a language with higher-type procedures. Acta Informatica, 20: 63–92.

    Article  MathSciNet  Google Scholar 

  • German, S. M., Clarke, E. M., and Halpern, J. Y. (1989). Reasoning about procedures as parameters in the language L4. Information and Computation, 83: 265–359.

    Article  MathSciNet  MATH  Google Scholar 

  • Goerdt, A. (1985). A Hoare calculus for functions defined by recursion on higher types. In (Parikh, 1985 ), pages 106–117.

    Google Scholar 

  • Hoare, C. A. R. (1969). An axiomatic basis for computer programming. Comm. ACM, 12(10):576–580 and 583.

    Google Scholar 

  • Hoare, C. A. R. (1971). Procedures and parameters: an axiomatic approach. In Symposium on Semantics of Algorithmic Languages (E. Engeler, editor), volume 188 of Lecture Notes in Mathematics, pages 102–116, Springer-Verlag, Berlin.

    Chapter  Google Scholar 

  • Meyer, A. R. and Sieber, K. (1988). Towards fully abstract semantics for local variables: preliminary report. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 191–203, ACM, New York. See Chapter 7.

    Google Scholar 

  • Milner, R., Morris, L., and Newey, M. (1975). A logic for computable functions with reflexive and polymorphic types. In Proving and Improving Programs ( G. Huet and G. Kahn, editors), pages 371–394, INRIA, Rocquencourt, France.

    Google Scholar 

  • Milner, R. (1972). Implementation and applications of Scott’s logic for computable functions. In Proc. of an ACM Conference on Proving Assertions About Programs, SIGPLAN Notices, 7(1) and SIGACT News, no. 14, pages 1–6, ACM, New York.

    Chapter  Google Scholar 

  • O’hearn, P. W. (1990). The Semantics of Non-Interference: A Natural Approach. Ph.D. thesis, Queen’s University, Kingston, Canada.

    Google Scholar 

  • Olderog, E. (1984a). Hoare’s logic for programs with procedures: what has been achieved? In Logics of Programs 1983 (E. M. Clarke, Jr. and D. Kozen, editors), volume 164 of Lecture Notes in Computer Science, pages 383–395, Springer-Verlag, Berlin, 1984.

    Google Scholar 

  • Olderog, E (1984b). Correctness of programs with PASCAL-like procedures without global variables. Theoretical Computer Science, 30: 49–90.

    Article  MathSciNet  MATH  Google Scholar 

  • Oles, F. J. (1982). A Category-Theoretic Approach to the Semantics of Programming Languages. Ph.D. thesis, Syracuse University, Syracuse, N.Y. See Chapter 11.

    Google Scholar 

  • Oles, F. J. (1985). Type algebras, functor categories and block structure. In Algebraic Methods in Semantics ( M. Nivat and J. C. Reynolds, editors), pages 543–573, Cambridge University Press, Cambridge, England. See Chapter 11.

    Google Scholar 

  • Parikh, R., editor (1985). Logics of Programs 1985, volume 193 of Lecture Notes in Computer Science, Springer-Verlag, Berlin.

    Google Scholar 

  • Plotkin, G. D. (1980) Lambda-definability in the full type hierarchy. In To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism (J. P. Seldin and J. R. Hindley, editors), pages 363–373, Academic Press.

    Google Scholar 

  • Reynolds, J. C. (1978). Syntactic control of interference. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 39–46, ACM, New York See Chapter 10.

    Google Scholar 

  • Reynolds, J. C. (1981a). The Craft of Programming. Prentice-Hall International, London.

    MATH  Google Scholar 

  • Reynolds, J. C. (198lb). The essence of ALGOL. In Algorithmic Languages,Proceedings of the International Symposium on Algorithmic Languages (J. W. de Bakker and J. C. van Vliet, editors), pages 345–372, North-Holland, Amsterdam. See Chapter 3.

    Google Scholar 

  • Reynolds, J. C. (1982). IDEALIZED ALGOL and its specification logic. In Tools and Notions for Program Construction (D. Néel, editor), pages 121–161, Cambridge University Press, Cambridge, 1982. See Chapter 6.

    Google Scholar 

  • Scott, D. S. (1969). A type-theoretical alternative to CucH, ISWIM, OWHY. Privately circulated memo, Oxford University. Published in Theoretical Computer Science, 121 (1/2): 411–440, 1993.

    Article  MathSciNet  MATH  Google Scholar 

  • Sieber, K. (1985). A partial correctness logic for procedures (in an ALGOL-like language). In (Parikh, 1985 ), pages 320–342.

    Google Scholar 

  • Statman, R. (1985). Logical relations and the typed A-calculus. Information and Computation, 65: 85–97.

    MathSciNet  MATH  Google Scholar 

  • Statman, R. (1990). Some models of Scott’s theory LCF based on a notion of rate of convergence. In Logic and Computation (W. Sieg, editor), volume 106 of Contemporary Mathematics, pages 263–80, American Mathematical Society, Providence, Rhode Island.

    Google Scholar 

  • Tennent, R. D. and Tobin, J. K. (1991). Continuations in possible-world semantics. Theoretical Computer Science, 85 (2): 283–303.

    Article  MathSciNet  MATH  Google Scholar 

  • Tennent, R. D. (1986). Functor-category semantics of programming languages and logics. In Category Theory and Computer Programming (D. Pitt, S. Abramsky, A. Poigné, and D. Rydeheard, editors), volume 240 of Lecture Notes in Computer Science, pages 206–224, Springer-Verlag, Berlin (1986).

    Chapter  Google Scholar 

  • Tennent, R. D. (1987). A note on undefined expression values in programming logics. Inf. Proc. Letters, 24: 331–333.

    Article  MathSciNet  MATH  Google Scholar 

  • Tennent, R. D. (1990). Semantical analysis of specification logic. Information and Computation,85(2):135–162. See Chapter 13.

    Google Scholar 

Download references

Authors
  1. Peter W. O’Hearn
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Robert D. Tennent
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dept. of Computer Science, Queen Mary & Westfield College, E1 4NS, England

    Peter W. O’Hearn

  2. Dept. of Computing and Information Science, Queen’s University, K7L 3N6, Kingston, Ontario, Canada

    Robert D. Tennent

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer Science+Business Media New York

About this chapter

Cite this chapter

O’Hearn, P.W., Tennent, R.D. (1997). Semantical Analysis of Specification Logic, 2. In: O’Hearn, P.W., Tennent, R.D. (eds) Algol-like Languages. Progress in Theoretical Computer Science. Birkhäuser, Boston, MA. https://doi.org/10.1007/978-1-4757-3851-3_4

Download citation

  • DOI: https://doi.org/10.1007/978-1-4757-3851-3_4

  • Publisher Name: Birkhäuser, Boston, MA

  • Print ISBN: 978-1-4757-3853-7

  • Online ISBN: 978-1-4757-3851-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation