Reusable Components of Semantic Specifications

  • Martin Churchill
  • Peter D. Mosses
  • Neil Sculthorpe
  • Paolo Torrini
Chapter

Abstract

Semantic specifications of programming languages typically have poor modularity. This hinders reuse of parts of the semantics of one language when specifying a different language – even when the two languages have many constructs in common – and evolution of a language may require major reformulation of its semantics. Such drawbacks have discouraged language developers from using formal semantics to document their designs.

In the PLanCompS project, we have developed a component-based approach to semantics. Here, we explain its modularity aspects, and present an illustrative case study: a component-based semantics for Caml Light. We have tested the correctness of the semantics by running programs on an interpreter generated from the semantics, comparing the output with that produced on the standard implementation of the language.

Our approach provides good modularity, facilitates reuse, and should support co-evolution of languages and their formal semantics. It could be particularly useful in connection with domain-specific languages and language-driven software development.

Keywords

Modularity Reusability Component-based semantics Fundamental constructs Funcons Modular SOS 

References

  1. 1.
    Afroozeh, A., van den Brand, M., Johnstone, A., Scott, E., Vinju, J.: Safe specification of operator precedence rules. In: Erwig, M., Paige, R.F., Van Wyk, E. (eds.) SLE 2013. LNCS, vol. 8225, pp. 137–156. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  2. 2.
    Bach Poulsen, C., Mosses, P.D.: Deriving pretty-big-step semantics from small-step semantics. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol. 8410, pp. 270–289. Springer, Heidelberg (2014) CrossRefGoogle Scholar
  3. 3.
    Poulsen, C.B., Mosses, P.D.: Generating Specialized Interpreters for Modular Structural Operational Semantics. In: Gupta, G., Peña, R. (eds.) LOPSTR 2013. LNCS, vol. 8901, pp. 220–236. Springer, Heidelberg (2014) CrossRefGoogle Scholar
  4. 4.
    Bergstra, J.A., Heering, J., Klint, P. (eds.): Algebraic Specification. ACM Press/Addison-Wesley, Reading (1989) MATHGoogle Scholar
  5. 5.
    Bogdănaş, D., Roşu, G.: K-Java: a complete semantics of Java. In: POPL 2015. ACM (2015)Google Scholar
  6. 6.
    Börger, E., Fruja, N.G., Gervasi, V., Stärk, R.F.: A high-level modular definition of the semantics of C#. Theor. Comput. Sci. 336(2–3), 235–284 (2005)CrossRefMATHGoogle Scholar
  7. 7.
    Börger, E., Stärk, R.F.: Exploiting abstraction for specification reuse: the Java/C# case study. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 42–76. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  8. 8.
    den van Brand, M.G.J., et al.: The ASF+SDF meta-environment: a component-based language development environment. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol. 2027, pp. 365–370. Springer, Heidelberg (2001) CrossRefGoogle Scholar
  9. 9.
    van den Brand, M.G.J., Iversen, J., Mosses, P.D.: An action environment. Sci. Comput. Program. 61(3), 245–264 (2006)CrossRefMATHGoogle Scholar
  10. 10.
    Chalub, F., Braga, C.: Maude MSOS tool. https://github.com/fcbr/mmt. Accessed Jan 2015
  11. 11.
    Churchill, M., Mosses, P.D.: Modular bisimulation theory for computations and values. In: Pfenning, F. (ed.) FOSSACS 2013 (ETAPS 2013). LNCS, vol. 7794, pp. 97–112. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  12. 12.
    Churchill, M., Mosses, P.D., Sculthorpe, N., Torrini, P.: Reusable components of semantic specifications: additional material (2015). http://www.plancomps.org/taosd2015
  13. 13.
    Churchill, M., Mosses, P.D., Torrini, P.: Reusable components of semantic specifications. In: Modularity 2014, pp. 145–156. ACM (2014)Google Scholar
  14. 14.
    Delaware, B., Keuchel, S., Schrijvers, T., Oliveira, B.C.: Modular monadic meta-theory. In: ICFP 2013, pp. 319–330. ACM (2013)Google Scholar
  15. 15.
    Doh, K.G., Mosses, P.D.: Composing programming languages by combining action-semantics modules. Sci. Comput. Program. 47(1), 3–36 (2003)CrossRefMATHGoogle Scholar
  16. 16.
    Doh, K.G., Schmidt, D.A.: Action semantics-directed prototyping. Comput. Lang. 19, 213–233 (1993)CrossRefGoogle Scholar
  17. 17.
    Ellison, C., Roşu, G.: An executable formal semantics of C with applications. In: POPL 2012, pp. 533–544. ACM (2012)Google Scholar
  18. 18.
    Felleisen, M., Findler, R.B., Flatt, M.: Semantics Engineering with PLT Redex. MIT Press, Cambridge (2009) MATHGoogle Scholar
  19. 19.
    Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103(2), 235–271 (1992)CrossRefMATHMathSciNetGoogle Scholar
  20. 20.
    Goguen, J.A., Malcolm, G.: Algebraic Semantics of Imperative Programs. MIT Press, Cambridge (1996) MATHGoogle Scholar
  21. 21.
    Harper, R., Stone, C.: A type-theoretic interpretation of Standard ML. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, Cambridge (2000)Google Scholar
  22. 22.
    Heering, J., Klint, P.: Prehistory of the ASF+SDF system (1980–1984). In: ASF+SDF95, pp. 1–4. Technical report 9504, Programming Research Group, University of Amsterdam (1995)Google Scholar
  23. 23.
    Hudak, P., Hughes, J., Jones, S.P., Wadler, P.: A history of Haskell: being lazy with class. In: HOPL-III, pp. 1–55. ACM (2007)Google Scholar
  24. 24.
    Iversen, J., Mosses, P.D.: Constructive action semantics for Core ML. Softw. IEE Proc. 152, 79–98 (2005). Special issue on Language Definitions and Tool GenerationCrossRefGoogle Scholar
  25. 25.
    Johnstone, A., Mosses, P.D., Scott, E.: An agile approach to language modelling and development. Innov. Syst. Softw. Eng. 6(1–2), 145–153 (2010). Special issue for ICFEM workshop FM+AM’09CrossRefGoogle Scholar
  26. 26.
    Johnstone, A., Scott, E.: Translator generation using ART. In: Malloy, B., Staab, S., van den Brand, M. (eds.) SLE 2010. LNCS, vol. 6563, pp. 306–315. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  27. 27.
    Kahn, G.: Natural semantics. In: Brandenburg, F.J., Vidal-Naquet, G., Wirsing, M. (eds.) STACS 87. LNCS, vol. 247, pp. 22–39. Springer, Heidelberg (1987) CrossRefGoogle Scholar
  28. 28.
    Kats, L.C.L., Visser, E.: The Spoofax language workbench. In: SPLASH/OOPSLA Companion, pp. 237–238. ACM (2010)Google Scholar
  29. 29.
    Klein, C., et al.: Run your research: on the effectiveness of lightweight mechanization. In: POPL 2012, pp. 285–296. ACM (2012)Google Scholar
  30. 30.
    Kutter, P.W., Pierantonio, A.: Montages specifications of realistic programming languages. J. Univ. Comput. Sci. 3(5), 416–442 (1997)MATHMathSciNetGoogle Scholar
  31. 31.
    Lee, D.K., Crary, K., Harper, R.: Towards a mechanized metatheory of Standard ML. In: POPL 2007, pp. 173–184. ACM (2007)Google Scholar
  32. 32.
    Leroy, X.: Caml Light manual, December 1997. http://caml.inria.fr/pub/docs/manual-caml-light
  33. 33.
    Levin, M.Y., Pierce, B.C.: TinkerType: a language for playing with formal systems. J. Funct. Program. 13(2), 295–316 (2003)CrossRefMATHMathSciNetGoogle Scholar
  34. 34.
    Lewis, J.R., Launchbury, J., Meijer, E., Shields, M.B.: Implicit parameters: dynamic scoping with static types. In: POPL 2000, pp. 108–118. ACM (2000)Google Scholar
  35. 35.
    Liang, S., Hudak, P., Jones, M.: Monad transformers and modular interpreters. In: POPL 1995, pp. 333–343 (1995)Google Scholar
  36. 36.
    McCarthy, J.: Towards a mathematical science of computation. In: Popplewell, C.M. (ed.) Information Processing 1962, pp. 21–28. North-Holland, Amsterdam (1962)Google Scholar
  37. 37.
    Meseguer, J., Roşu, G.: The rewriting logic semantics project: a progress report. In: Owe, O., Steffen, M., Telle, J.A. (eds.) FCT 2011. LNCS, vol. 6914, pp. 1–37. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  38. 38.
    Milner, R., Tofte, M., Macqueen, D.: The Definition of Standard ML. MIT Press, Cambridge (1997) Google Scholar
  39. 39.
    Moggi, E.: An abstract view of programming languages. Technical report ECS-LFCS-90-113, Edinburgh University (1989)Google Scholar
  40. 40.
    Mosses, P.D.: Action Semantics, Cambridge Tracts in Theoretical Computer Science, vol. 26. Cambridge University Press, Cambridge (1992)Google Scholar
  41. 41.
    Mosses, P.D.: Theory and practice of action semantics. In: Penczek, W., Szałas, A. (eds.) MFCS 1996. LNCS, vol. 1113, pp. 37–61. Springer, Heidelberg (1996) CrossRefGoogle Scholar
  42. 42.
    Mosses, P.D.: Modular structural operational semantics. J. Log. Algebr. Program. 60–61, 195–228 (2004)CrossRefMathSciNetGoogle Scholar
  43. 43.
    Mosses, P.D.: A constructive approach to language definition. J. Univ. Comput. Sci. 11(7), 1117–1134 (2005)Google Scholar
  44. 44.
    Mosses, P.D.: Teaching semantics of programming languages with Modular SOS. In: Teaching Formal Methods: Practice and Experience. Electronic Workshops in Computing. BCS (2006)Google Scholar
  45. 45.
    Mosses, P.D.: Component-based description of programming languages. In: Visions of Computer Science. Electronic Proceedings, pp. 275–286. BCS (2008)Google Scholar
  46. 46.
    Mosses, P.D.: Component-based semantics. In: SAVCBS 2009, pp. 3–10. ACM (2009)Google Scholar
  47. 47.
    Mosses, P.D.: VDM semantics of programming languages: combinators and monads. Form. Asp. Comput. 23, 221–238 (2011)CrossRefMATHMathSciNetGoogle Scholar
  48. 48.
    Mosses, P.D.: Semantics of programming languages: using ASF+SDF. Sci. Comput. Program. 97(1), 2–10 (2013). http://dx.doi.org/10.1016/j.scico.2013.11.038 Google Scholar
  49. 49.
    Mosses, P.D., New, M.J.: Implicit propagation in structural operational semantics. In: SOS 2008. Electr. Notes Theor. Comput. Sci., vol. 229(4), pp. 49–66. Elsevier (2009)Google Scholar
  50. 50.
    Mosses, P.D., Vesely, F.: FunKons: component-based semantics in K. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 213–229. Springer, Heidelberg (2014) CrossRefGoogle Scholar
  51. 51.
    Mosses, P.D., Watt, D.A.: The use of action semantics. In: Formal Description of Programming Concepts III, Proceedings of IFIP TC2 Working Conference, Gl. Avernæs, 1986, pp. 135–166. Elsevier (1987)Google Scholar
  52. 52.
    Owens, S., Peskine, G., Sewell, P.: A formal specification for OCaml: the core language. Technical report, University of Cambridge (2008)Google Scholar
  53. 53.
    Owens, S.: A sound semantics for OCaml light. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 1–15. Springer, Heidelberg (2008) CrossRefGoogle Scholar
  54. 54.
    Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002) Google Scholar
  55. 55.
    PLanCompS: Programming language components and specifications (2011). http://www.plancomps.org
  56. 56.
    Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebr. Program. 60–61, 17–139 (2004)MathSciNetGoogle Scholar
  57. 57.
    Plotkin, G.D., Power, A.J.: Computational effects and operations: an overview. In: Proceedings of Workshop on Domains VI. Electr. Notes Theor. Comput. Sci., vol. 73, pp. 149–163. Elsevier (2004)Google Scholar
  58. 58.
    Roşu, G., Şerbănuţă, T.F.: K overview and SIMPLE case study. Electr. Notes Theor. Comput. Sci. 304, 3–56 (2014)CrossRefGoogle Scholar
  59. 59.
    Sewell, P., Nardelli, F.Z., Owens, S., et al.: Ott: effective tool support for the working semanticist. J. Funct. Program. 20, 71–122 (2010)CrossRefMATHGoogle Scholar
  60. 60.
    Tofte, M.: Type inference for polymorphic references. Inf. Comput. 89(1), 1–34 (1990)CrossRefMATHMathSciNetGoogle Scholar
  61. 61.
    Visser, E.: Syntax Definition for Language Prototyping. Ph.D. thesis, University of Amsterdam (1997)Google Scholar
  62. 62.
    Visser, E.: Stratego: a language for program transformation based on rewriting strategies system description of Stratego 0.5. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 357–361. Springer, Heidelberg (2001) CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  • Martin Churchill
    • 1
  • Peter D. Mosses
    • 2
  • Neil Sculthorpe
    • 2
  • Paolo Torrini
    • 2
  1. 1.Google, Inc.LondonUK
  2. 2.PLanCompS ProjectSwansea UniversitySwanseaUK

Personalised recommendations