Skip to main content
SpringerLink
Log in

Semantical Analysis of Specification Logic

  • Chapter
Algol-like Languages

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

  • 122 Accesses

Abstract

The specification logic of J. C. Reynolds is a partial-correctness logic for Algol 60-like languages with procedures. It is interpreted here as an intuitionistic theory, using a form of possible-world semantics first applied to programming-language interpretation by Reynolds and F. J. Oles to give an abstract treatment of stack-oriented storage management. The model provides a satisfactory solution to all previously-known problems with the interpretation of specification logic; however, unexpected new problems have been discovered in doing this work, and these remain unsolved.

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

  • Arbib, M. A. And Alagic, S. (1979). Proof rules for gotos. Acta Informatica, 11: 139148.

    Google Scholar 

  • Bencivenga, E. (1986). Free logics. In Handbook of Philosophical Logic, vol. Iii: Alternatives in Classical Logic (D. Gabbay and F. Guenthner, editors), number 166 in Synthese Library, pages 373–426, D. Reidel, Dordrecht, Holland.

    Google Scholar 

  • Bergstra, J. A., Tiuryn, J., And Tucker, J. (1982). Floyd’s principle, correctness the- ories, and program equivalence. Theoretical Computer Science, 17: 129–147.

    Google Scholar 

  • Clarke, JR., E. M. And KozEN, D., editors (1984). Logics of Programs 1983, volume 164 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1984.

    Google Scholar 

  • Clarke, JR. E. M. (1984). The characterization problem for Hoare logics. In Mathematical Logic and Programming Languages (C. A. R. Hoare and J. C. Shepherdson, editors), pages 89–106, Prentice-Hall International.

    Google Scholar 

  • Clint, M. And Hoare, C. A. R. (1972). Program proving: jumps and functions. Acta Informatica, 1:214–224.

    Google Scholar 

  • CooK, S. A. (1978). Soundness and completeness of an axiomatic system for program verification. Siam J. on Computing, 7:70–90. Corrigendum,10: 612 (1981).

    Google Scholar 

  • DE Bakker, J. W. And Meertens, L. G. L. T. (1975). On the completeness of the inductive assertion method. J. Comput. Sys. Sci., 11: 323–357.

    Article  MATH  Google Scholar 

  • DE Bakker, J. W., DE Bruin, A., And Zucker, J. I. (1980). Mathematical Theory of Program Correctness. Prentice-Hall International, London.

    MATH  Google Scholar 

  • Dummett, M. (1977). Elements of Intuitionism. Oxford University Press.

    Google Scholar 

  • Goldblatt, R. (1979). Topoi, The Categorial Analysis of Logic. North-Holland, Amsterdam.

    MATH  Google Scholar 

  • Goldblatt, R. (1982). Axiomatising the Logic of Computer Programming, volume 193 of Lecture Notes in Computer Science. Springer-Verlag, Berlin.

    Google Scholar 

  • Gries, D. and Levin, G. (1980). Assignment and procedure call proof rules. Acm Trans. on Programming Languages and Systems, 2 (4): 564–579.

    Article  MathSciNet  MATH  Google Scholar 

  • Gries, D., editor (1978). Programming Methodology, A Collection of Articles by Ifip WG 2.3. Springer-Verlag, New York.

    Google Scholar 

  • Hoare, C. A. R. And Lauer, P. E. (1974). Consistent and complementary formal theories of the semantics of programming languages. Acta Informatica, 3 (2): 135–153.

    Article  MathSciNet  MATH  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 

  • Hoare, C. A. R. (1972). Proof of correctness of data representations. Acta Informatica, 1:271–281. Reprinted in (Gries, 1978 ), pages 269–281.

    Google Scholar 

  • Kripke, S. A. (1965) Semantical analysis of intuitionistic logic I. In Formal Systems and Recursive Functions (J. N. Crossley and M. A. E. Dummett, editors), pages 92–130, North-Holland, Amsterdam

    Chapter  Google Scholar 

  • Lambek, J. And Scott, P. J. (1986). Introduction to Higher-Order Categorical Logic. Cambridge University Press, Cambridge, England.

    Google Scholar 

  • Lambek, J. (1980). From lambda-calculus to cartesian-closed categories. In (Seldin and Hindley, 1980 ), pages 375–402.

    Google Scholar 

  • Leivant, D. And Fernando, T. (1987). Skinny and fleshy failures of relative completeness. In Con f. Record 14th Acm Symp. on Principles of Programming Languages, pages 246–252, Acm, New York.

    Google Scholar 

  • Leivant, D. (1985). Logical and mathematical reasoning about imperative programs. In Con f. Record 12th Acm Symp. on Principles of Programming Languages, pages 132–140, Acm, New York.

    Google Scholar 

  • Mccarty, C. (1984). Information systems, continuity, and realizability. In (Clarke and Kozen, 1984 ), pages 341–359.

    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 

  • Olderog, E. (1984). Hoare’s logic for programs with procedures: what has been achieved? In (Clarke and Kozen, 1984 ), pages 383–395.

    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.

    Google Scholar 

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

    Google Scholar 

  • Pasztor, A. (1986). Non-standard algorithmic and dynamic logic. J. Symbolic Computation, 2: 59–81.

    Article  MathSciNet  MATH  Google Scholar 

  • Plotkin, G. D. (1985). Types and partial functions. Lecture notes, Computer Science Department, University of Edinburgh.

    Google Scholar 

  • Reynolds, J. C. (1977). Semantics of the domain of flow diagrams. J. Acm, 24(3): 484503.

    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. (1980). Using category theory to design implicit conversions and generic operators. In Semantics-Directed Compiler Generation (N. D. Jones, editor), volume 94 of Lecture Notes in Computer Science, pages 211–258, Springer-Verlag, Berlin.

    Chapter  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. (1967). Existence and description in formal logic. In Bertrand Russell, Philosopher of the Century ( R. Schönmann, editor), pages 181–200, Allen and Unwin, London.

    Google Scholar 

  • Score, D. S. (1979). Identity and existence in intuitionistic logic. In Applications of Sheaves (M. P. Fourman, C. V. Mulvey, and D. S. Scott, editors), volume 735 of Lecture Notes in Mathematics, pages 660–696, Springer-Verlag, Berlin.

    Google Scholar 

  • Scott, D. S. (1980). Relating theories of the lambda calculus. In (Seldin and Hindley, 1980 ), pages 403–450.

    Google Scholar 

  • Seldin, J. P. And Hindley, J. R., editors (1980). To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism. Academic Press.

    Google Scholar 

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

    Google Scholar 

  • Stoughton, A. (1988). Fully Abstract Models of Programming Languages. Research Notes in Theoretical Computer Science, Pitman, London, and Wiley, New York.

    Google Scholar 

  • Tennent, R. D. (1985). Semantical analysis of specification logic (preliminary report). In (Parikh, 1985 ), pages 373–386.

    Google Scholar 

  • Trakhtenbrot, B. A., Halpern, J. Y., And Meyer, A. R. (1983). From denotational to operational and axiomatic semantics for Algol-like languages: an overview. In (Clarke and Kozen, 1984 ), pages 474–500.

    Google Scholar 

  • Van Dalen, D. (1983). Logic and Structure. Springer, Berlin, second edition.

    Google Scholar 

  • Wand, M. (1978). A new incompleteness result for Hoare’s system. J. Acm, 25: 168175.

    Google Scholar 

Download references

Authors
  1. 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

Tennent, R.D. (1997). Semantical Analysis of Specification Logic. 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_3

Download citation

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

  • 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