Skip to main content
SpringerLink
Log in

Understanding Programming Language Concepts Via Operational Semantics

  • Chapter
Domain Modeling and the Duration Calculus

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4710))

Abstract

The origins of “formal methods” lie partly in language description (although applications of methods like VDM, RAISE or B to areas other than programming languages are probably more widely known). This paper revisits the language description task but uses operational (rather than denotational) semantics to illustrate that the crucial idea is thinking about an abstract model of something that one is trying to understand or design. A “story” is told which links together some of the more important concepts in programming languages and thus illustrates how formal semantics deepens our understanding.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight 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

  1. Allen, C.D., Chapman, D.N., Jones, C.B.: A formal definition of ALGOL 60. Technical Report 12.105, IBM Laboratory Hursley (August 1972)

    Google Scholar 

  2. America, P.: Issues in the design of a parallel object-oriented language. Formal Aspects of Computing 1(4) (1989)

    Google Scholar 

  3. Backus, J.W., Bauer, F.L., Green, J., Katz, C., McCarthy, J., Naur, P., Perlis, A.J., Rutishauser, H., Samelson, K., Vauquois, B., Wegstein, J.H., van Wijngaarden, A., Woodger, M.: Revised report on the algorithmic language Algol 60. Communications of the ACM 6(1), 1–17 (1963)

    Article  Google Scholar 

  4. Bekič, H., Bjørner, D., Henhapl, W., Jones, C.B., Lucas, P.: A formal definition of a PL/I subset. Technical Report 25.139, IBM Laboratory Vienna (December 1974)

    Google Scholar 

  5. Bjørner, D., Jones, C.B. (eds.): The Vienna Development Method: The Meta-Language. LNCS, vol. 61. Springer, Heidelberg (1978)

    MATH  Google Scholar 

  6. Bjørner, D., Jones, C.B.: Formal Specification and Software Development. Prentice Hall International, Englewood Cliffs (1982)

    MATH  Google Scholar 

  7. Boole, G.: An Investigation of the Laws of Thought. Macmillan (1854) (reprinted by Dover (1958))

    Google Scholar 

  8. Butler, M.J.: CSP2B: A practical approach to combining CSP and B. Formal Aspects of Computing 12(3), 182–198 (2000)

    Article  MATH  Google Scholar 

  9. Coleman, J.W., Jones, C.B.: Guaranteeing the soundness of rely/guarantee rules (revised). Journal of Logic and Computation (accepted for publication, 2007)

    Google Scholar 

  10. Coleman, J.W., Jefferson, N.P., Jones, C.B.: Comments on several years of teaching of modelling programming language concepts. Technical Report CS-TR-978, Newcastle University (2006)

    Google Scholar 

  11. Camilleri, J., Melham, T.: Reasoning with inductively defined relations in the HOL theorem prover. Technical Report 265, Computer Laboratory, University of Cambridge (August 1992)

    Google Scholar 

  12. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

  13. D’Souza, D.F., Wills, A.C.: Objects, components, and frameworks with UML: the catalysis approach. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA (1999)

    Google Scholar 

  14. Engeler, E.: Symposium on Semantics of Algorithmic Languages. Lecture Notes in Mathematics, vol. 188. Springer, Heidelberg (1971)

    MATH  Google Scholar 

  15. Fitzgerald, J., GormLarsen, P.: Modelling systems: practical tools and techniques in software development. Cambridge University Press, Cambridge (1998)

    Google Scholar 

  16. Gordon, M.J.C.: The Denotational Description of Programming Languages: An Introduction. Springer, Heidelberg (1979)

    MATH  Google Scholar 

  17. Gordon, M.J.C.: Programming Language Theory and its Implementation. Prentice-Hall International, Englewood Cliffs (1988)

    Google Scholar 

  18. Hennessy, M.: The Semantics of Programming Languages: an elementary introduction using structural operational semantics. Wiley, Chichester (1990)

    MATH  Google Scholar 

  19. Henhapl, W., Jones, C.B.: On the interpretation of GOTO statements in the ULD. Technical Report LN 25.3.065, IBM Laboratory, Vienna (March 1970)

    Google Scholar 

  20. Henhapl, W., Jones, C.B.: A run-time mechanism for referencing variables. Information Processing Letters 1, 14–16 (1971)

    Article  MATH  Google Scholar 

  21. Hoare, C.A.R.: Communicating sequential processes. Communications of the ACM 21, 666–677 (1978)

    Article  MATH  Google Scholar 

  22. Jones, C.B., Lucas, P.: Proving correctness of implementation techniques. In: [Eng71], pp. 178–211 (1971)

    Google Scholar 

  23. Jones, C.B., Lomet, D., Romanovsky, A., Weikum, G.: The atomicity manifesto (2005)

    Google Scholar 

  24. Jones, C.B.: A pi-calculus semantics for an object-based design notation. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 158–172. Springer, Heidelberg (1993)

    Google Scholar 

  25. Jones, C.B.: Process algebra arguments about an object-based design notation. In: Classical, A. (ed.) A Classical Mind: Essays in Honour of C. A. R. Hoare, ch. 14, Prentice-Hall, Englewood Cliffs (1994)

    Google Scholar 

  26. Jones, C.B.: Accommodating interference in the formal design of concurrent object-based programs. Formal Methods in System Design 8(2), 105–122 (1996)

    Article  Google Scholar 

  27. Jones, C.B.: On the search for tractable ways of reasoning about programs. Technical Report CS-TR-740, Newcastle University, Superceded by [Jon03a] (2001)

    Google Scholar 

  28. Jones, C.B.: The transition from VDL to VDM. JUCS 7(8), 631–640 (2001)

    MATH  Google Scholar 

  29. Jones, C.B.: The early search for tractable ways of reasonning about programs. IEEE, Annals of the History of Computing 25(2), 26–49 (2003)

    Article  MathSciNet  Google Scholar 

  30. Jones, C.B.: Operational semantics: concepts and their expression. Information Processing Letters 88(1-2), 27–32 (2003)

    Article  MathSciNet  Google Scholar 

  31. Klein, G., Nipkow, T., von Oheimb, D., Nieto, L.P., Schirmer, N., Strecker, M.: Java source and bytecode formalisations in Isabelle (2002)

    Google Scholar 

  32. Liskov, B.: A history of CLU. In: History of programming languages—II, pp. 471–510. ACM Press, New York (1996)

    Google Scholar 

  33. Lucas, P., Walk, K.: On The Formal Description of PL/I. In: Annual Review in Automatic Programming Part 3, vol.  6, Pergamon Press, Oxford (1969)

    Google Scholar 

  34. McCarthy, J.: A formal description of a subset of ALGOL. In: [Ste66], pp. 1–12 (1966)

    Google Scholar 

  35. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  36. Mosses, P.D.: Action Semantics. Cambridge Tracts in Theoretical Computer Science, vol. 26. Cambridge University Press, Cambridge (1992)

    MATH  Google Scholar 

  37. Mosses, P.D.: Teaching semantics of programming languages with Modular SOS. In: Teaching Formal Methods: Practice and Experience. Electr. Workshops in Comput. BCS (2006)

    Google Scholar 

  38. McCarthy, J., Painter, J.: Correctness of a compiler for arithmetic expressions. Technical Report CS38, Computer Science Department, Stanford University (April 1966) (see also Proc. Symp. in Applied Mathematics, vol.19, pp. 33–41, Mathematical Aspects of Computer Science, American Mathematical Society (1967))

    Google Scholar 

  39. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. Information and Computation 100, 1–77 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  40. Nielson, H.R., Nielson, F.: Semantics with Applications: A Formal Introduction. Wiley, Chichester (1992), available on the WWW as http://www.daimi.au.dk/bra8130/Wiley_book/wiley.html

    MATH  Google Scholar 

  41. Plotkin, G.D.: A structural approach to operational semantics. Technical report, Aarhus University (1981)

    Google Scholar 

  42. Plotkin, G.D.: The origins of structural operational semantics. Journal of Logic and Algebraic Programming 60–61, 3–15 (July–December, 2004)

    Article  MathSciNet  Google Scholar 

  43. Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60–61, 17–139 (July–December, 2004)

    MathSciNet  Google Scholar 

  44. Reynolds, J.C.: Theories of Programming Languages. Cambridge University Press, Cambridge (1998)

    MATH  Google Scholar 

  45. Sangiorgi, D.: Typed π-calculus at work: a correctness proof of Jones’s parallelisation transformation on concurrent objects. Theory and Practice of Object Systems 5(1), 25–34 (1999)

    Article  MathSciNet  Google Scholar 

  46. Scott, M.L.: Programming Language Pragmatics. Morgan Kaufmann, San Francisco (2000)

    Google Scholar 

  47. Steel, T.B.: Formal Language Description Languages for Computer Programming. North-Holland, Amsterdam (1966)

    Google Scholar 

  48. Stoy, J.E.: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge (1977)

    Google Scholar 

  49. Sangiorgi, D., Walker, D.: The π-calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)

    Google Scholar 

  50. van Wijngaarden, A., Sintzoff, M., Mailloux, B.J., Lindsey, C.H., Peck, J.E.L., Meertens, L.G.L.T., Koster, C.H.A., Fisker, R.G.: Revised report on the Algorithmic Language ALGOL 68, Mathematisch Centrum, Amsterdam. Mathematical Centre Tracts 50 (1976)

    Google Scholar 

  51. Walker, D.: π-calculus semantics for object-oriented programming languages. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 532–547. Springer, Heidelberg (1991)

    Google Scholar 

  52. Walker, D.: Process calculus and parallel object-oriented programming languages. In: Casavant, T. (ed.) Parallel Computers: Theory and Practice, Computer Society Press (1993)

    Google Scholar 

  53. Watt, D.A.: Programming Language Design Concepts. John Wiley, Chichester (2004)

    Google Scholar 

  54. Woodcock, J., Cavalcanti, A.: The semantics of circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  55. Wexelblat, R.L. (ed.): History of Programming Languages. Academic Press, London (1981)

    MATH  Google Scholar 

  56. Wirth, N., Hoare, C.A.R.: A contribution to the development of algol. Commun. ACM 9(6), 413–432 (1966)

    Article  MATH  Google Scholar 

  57. Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)

    MATH  Google Scholar 

  58. Zemanek, H.: Semiotics and programming languages. Communications of the ACM 9, 139–143 (1966)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computing Science, University of Newcastle, NE1 7RU, UK

    Cliff B. Jones

Authors
  1. Cliff B. Jones
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Chris W. George Zhiming Liu Jim Woodcock

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Jones, C.B. (2007). Understanding Programming Language Concepts Via Operational Semantics. In: George, C.W., Liu, Z., Woodcock, J. (eds) Domain Modeling and the Duration Calculus. Lecture Notes in Computer Science, vol 4710. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74964-6_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74964-6_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74963-9

  • Online ISBN: 978-3-540-74964-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation