No Cover Image

Journal article 753 views 197 downloads

Executable component-based semantics

L. Thomas van Binsbergen, Peter Mosses Orcid Logo, Neil Sculthorpe

Journal of Logical and Algebraic Methods in Programming, Volume: 103, Pages: 184 - 212

Swansea University Author: Peter Mosses Orcid Logo

  • preprintv4.pdf

    PDF | Accepted Manuscript

    Released under the terms of a Creative Commons Attribution Non-Commercial No Derivatives License (CC-BY-NC-ND).

    Download (1021.85KB)

Check full text

DOI (Published version): 10.1016/j.jlamp.2018.12.004

Abstract

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 invest...

Full description

Published in: Journal of Logical and Algebraic Methods in Programming
ISSN: 23522208
Published: 2019
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa48792
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2019-02-11T20:04:25Z
last_indexed 2019-02-21T20:05:40Z
id cronfa48792
recordtype SURis
fullrecord <?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>48792</id><entry>2019-02-11</entry><title>Executable component-based semantics</title><swanseaauthors><author><sid>3f13b8ec315845c81d371f41e772399c</sid><ORCID>0000-0002-5826-7520</ORCID><firstname>Peter</firstname><surname>Mosses</surname><name>Peter Mosses</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2019-02-11</date><deptcode>FGSEN</deptcode><abstract>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.</abstract><type>Journal Article</type><journal>Journal of Logical and Algebraic Methods in Programming</journal><volume>103</volume><journalNumber/><paginationStart>184</paginationStart><paginationEnd>212</paginationEnd><publisher/><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint>23522208</issnPrint><issnElectronic/><keywords>programming languages, formal semantics, reuse, components, tool support</keywords><publishedDay>28</publishedDay><publishedMonth>2</publishedMonth><publishedYear>2019</publishedYear><publishedDate>2019-02-28</publishedDate><doi>10.1016/j.jlamp.2018.12.004</doi><url/><notes/><college>COLLEGE NANME</college><department>Science and Engineering - Faculty</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>FGSEN</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2023-06-23T15:46:36.5153118</lastEdited><Created>2019-02-11T15:02:15.3299094</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2"/></path><authors><author><firstname>L. Thomas van</firstname><surname>Binsbergen</surname><order>1</order></author><author><firstname>Peter</firstname><surname>Mosses</surname><orcid>0000-0002-5826-7520</orcid><order>2</order></author><author><firstname>Neil</firstname><surname>Sculthorpe</surname><order>3</order></author></authors><documents><document><filename>0048792-21022019150920.pdf</filename><originalFilename>preprintv4.pdf</originalFilename><uploaded>2019-02-21T15:09:20.9430000</uploaded><type>Output</type><contentLength>993926</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><embargoDate>2020-01-04T00:00:00.0000000</embargoDate><documentNotes>Released under the terms of a Creative Commons Attribution Non-Commercial No Derivatives License (CC-BY-NC-ND).</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling v2 48792 2019-02-11 Executable component-based semantics 3f13b8ec315845c81d371f41e772399c 0000-0002-5826-7520 Peter Mosses Peter Mosses true false 2019-02-11 FGSEN 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. Journal Article Journal of Logical and Algebraic Methods in Programming 103 184 212 23522208 programming languages, formal semantics, reuse, components, tool support 28 2 2019 2019-02-28 10.1016/j.jlamp.2018.12.004 COLLEGE NANME Science and Engineering - Faculty COLLEGE CODE FGSEN Swansea University 2023-06-23T15:46:36.5153118 2019-02-11T15:02:15.3299094 Faculty of Science and Engineering L. Thomas van Binsbergen 1 Peter Mosses 0000-0002-5826-7520 2 Neil Sculthorpe 3 0048792-21022019150920.pdf preprintv4.pdf 2019-02-21T15:09:20.9430000 Output 993926 application/pdf Accepted Manuscript true 2020-01-04T00:00:00.0000000 Released under the terms of a Creative Commons Attribution Non-Commercial No Derivatives License (CC-BY-NC-ND). true eng
title Executable component-based semantics
spellingShingle Executable component-based semantics
Peter Mosses
title_short Executable component-based semantics
title_full Executable component-based semantics
title_fullStr Executable component-based semantics
title_full_unstemmed Executable component-based semantics
title_sort Executable component-based semantics
author_id_str_mv 3f13b8ec315845c81d371f41e772399c
author_id_fullname_str_mv 3f13b8ec315845c81d371f41e772399c_***_Peter Mosses
author Peter Mosses
author2 L. Thomas van Binsbergen
Peter Mosses
Neil Sculthorpe
format Journal article
container_title Journal of Logical and Algebraic Methods in Programming
container_volume 103
container_start_page 184
publishDate 2019
institution Swansea University
issn 23522208
doi_str_mv 10.1016/j.jlamp.2018.12.004
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
document_store_str 1
active_str 0
description 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.
published_date 2019-02-28T15:46:31Z
_version_ 1769505126344556544
score 10.998093

Similar Items