Abstract
We are presenting a semantic analysis of Reynolds’s specification logic of Idealized Algol using the parametric operational techniques developed by Pitts. We hope that this more elementary account will make the insights of Tennent and O’Hearn, originally formulated in a functor-category denotational semantics, more accessible to a wider audience. The operational model makes clearer the special nature of term equivalence in the logical setting, identifies some problems in the previous interpretation of negation and also proves the soundness of two new axioms of specification logic. Using the model we show that even a very restricted fragment of specification logic is undecidable.
Chapter PDF
References
Reynolds, J.C.: The Craft of Programming. Prentice-Hall Intl., London (1981)
Reynolds, J.C.: Idealized Algol and its specification logic. In: Néel, D. (ed.) Tools and Notions for Program Construction, Nice, France, pp. 121–161. Cambridge University Press, Cambridge 1982 (1981); Also [7, Chap. 6]
Tennent, R.D.: Semantical analysis of specification logic. Information and Computation 85, 135–162 (1990); Also [7, Chap. 13]
Reynolds, J.C.: The essence of Algol. In: de Bakker, J.W., van Vliet, J.C. (eds.) Algorithmic Languages, Proceedings of the International Symposium on Algorithmic Languages, Amsterdam, pp. 345–372 (1981); Also [7, Chap. 3]
Oles, F.J.: Functor categories and store shapes. In: [7, Chap. 11], pp. 3–12
O’Hearn, P.W., Tennent, R.D.: Semantical analysis of specification logic, 2. Information and Computation 107, 25–57 (1993); Also [7, Chap. 19]
O’Hearn, P.W., Tennent, R.D. (eds.): Algol-like Languages. Progress in Theoretical Computer Science. Birkhäuser, Boston (1997), Two volumes
Pitts, A.M.: Reasoning about local variables with operationally-based logical relations. In: Proceedings of LICS 11, Washington, pp. 152–163 (1996); Also [7, Chap. 17]
O’Hearn, P.W.: The Semantics of Non-Interference: A Natural Approach. Ph.D. thesis, Queen’s University, Kingston, Canada (1990)
Launchbury, J., Peyton Jones, S.: State in Haskell. Lisp and Symbolic Computation 8, 293–341 (1995)
Ghica, D.R., McCusker, G.: Reasoning about Idealized algol using regular languages. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 103–116. Springer, Heidelberg (2000)
Ong, C.H.L.: Observational equivalence of third-order Idealized Algol is decidable. In: Proceedings of LICS 17, Copenhagen, pp. 22–25 (2002)
O’Hearn, P.W.: Note on Algol and conservatively extending functional programming. J. of Functional Programming 6, 171–180 (1995); Also [7, Chap. 4]
Milner, R.: Fully abstract models of typed λ-calculi. Theoretical Computer Science 4, 1–22 (1977)
van Dalen, D.: Logic and Structure, 3rd edn. Springer, Berlin (1994)
Bencivenga, E.: Free logics. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. III: Alternatives in Classical Logic. Synthese Library, vol. 166, pp. 373–426. D. Reidel, Dordrecht (1986)
Matiyasevich, Y.V.: Hilbert’s tenth Problem. Nauka Publishers, Fizmalit (1993), English translation: MIT Press, Cambridge, MA (1993)
Mason, I.A., Talcott, C.L.: References, local variables, and operational reasoning. In: Proceedings of LICS 7, Santa Cruz, California, pp. 186–197 (1992)
Honsell, F., Mason, I., Smith, S., Talcott, C.: A variable typed logic of effects. Information and Computation 119, 55–90 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ghica, D.R. (2004). Semantical Analysis of Specification Logic, 3. In: Schmidt, D. (eds) Programming Languages and Systems. ESOP 2004. Lecture Notes in Computer Science, vol 2986. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24725-8_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-24725-8_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21313-0
Online ISBN: 978-3-540-24725-8
eBook Packages: Springer Book Archive