Executable component-based semantics

被引:9
作者
van Binsbergen, L. Thomas [1 ]
Mosses, Peter D. [2 ,3 ]
Sculthorpe, Neil [4 ]
机构
[1] Royal Holloway Univ London, Dept Comp Sci, Egham TW20 0EX, Surrey, England
[2] Swansea Univ, Dept Comp Sci, Swansea SA2 8PP, W Glam, Wales
[3] Delft Univ Technol, EEMCS, Programming Languages, POB 5031, NL-2600 GA Delft, Netherlands
[4] Nottingham Trent Univ, Dept Comp & Technol, Nottingham NG11 8NS, England
基金
英国工程与自然科学研究理事会;
关键词
Programming languages; Formal semantics; Reuse; Components; Tool support; SPECIFICATION; MAUDE;
D O I
10.1016/j.jlamp.2018.12.004
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
The potential benefits of formal semantics are well known. However, a substantial amount of work is required to produce a complete and accurate formal semantics for a major language; and when the language evolves, large-scale revision of the semantics may be needed to reflect the changes. The investment of effort needed to produce an initial definition, and subsequently to revise it, has discouraged language developers from using formal semantics. Consequently, many major programming languages (and most domain-specific languages) do not yet have formal semantic definitions. To improve the practicality of formal semantic definitions, the PLANCOMPS project has developed a component-based approach. In this approach, the semantics of a language is defined by translating its constructs (compositionally) to combinations of so-called fundamental constructs, or 'funcons'. Each funcon is defined using a modular variant of Structural Operational Semantics, and forms a language-independent component that can be reused in definitions of different languages. A substantial library of funcons has been developed and tested in several case studies. Crucially, the definition of each funcon is fixed, and does not need changing when new funcons are added to the library. For specifying component-based semantics, we have designed and implemented a meta-language called CBS. It includes specification of abstract syntax, of its translation to funcons, and of the funcons themselves. Development of CBS specifications is supported by an integrated development environment. The accuracy of a language definition can be tested by executing the specified translation on programs written in the defined language, and then executing the resulting funcon terms using an interpreter generated from the CBS definitions of the funcons. This paper gives an introduction to CBS, illustrates its use, and presents the various tools involved in our implementation of CBS. (C) 2019 Elsevier Inc. All rights reserved.
引用
收藏
页码:184 / 212
页数:29
相关论文
共 43 条
  • [1] [Anonymous], 1987, The Implementation of Functional Programming Languages
  • [2] [Anonymous], 2018, PLANCOMPS PROJ CBS F
  • [3] MAIN FEATURES OF CPL
    BARRON, DW
    BUXTON, JN
    NIXON, E
    STRACHEY, C
    HARTLEY, DF
    [J]. COMPUTER JOURNAL, 1963, 6 (02) : 134 - &
  • [4] Maude MSOS Tool
    Chalub, Fabricio
    Braga, Christiano
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 176 (04) : 133 - 146
  • [5] Reusable Components of Semantic Specifications
    Churchill, Martin
    Mosses, Peter D.
    Sculthorpe, Neil
    Torrini, Paolo
    [J]. TRANSACTIONS ON ASPECT-ORIENTED SOFTWARE DEVELOPMENT XII, 2015, 8989 : 132 - 179
  • [6] Churchill M, 2013, LECT NOTES COMPUT SC, V7794, P97, DOI 10.1007/978-3-642-37075-5_7
  • [7] Maude:: Specification and programming in rewriting logic
    Clavel, M
    Durán, F
    Eker, S
    Lincoln, P
    Martí-Oliet, N
    Meseguer, J
    Quesada, JF
    [J]. THEORETICAL COMPUTER SCIENCE, 2002, 285 (02) : 187 - 243
  • [8] Danvy O., 1989, 8912 DIKU U COP
  • [9] Day Laurence E., 2012, Trends in Functional Programming. 12th International Symposium, TFP 2011. Revised Selected Papers, P49, DOI 10.1007/978-3-642-32037-8_4
  • [10] Degueule Thomas., 2015, SLE 2015 P 2015 ACM, P25, DOI DOI 10.1145/2814251.2814252