No Cover Image

Conference Paper/Proceeding/Abstract 792 views

Implicit propagation in structural operational semantics

Peter Mosses Orcid Logo, Mark J New

Electronic Notes in Theoretical Computer Science, Volume: 229, Issue: 4, Pages: 49 - 66

Swansea University Author: Peter Mosses Orcid Logo

Full text not available from this repository: check for access using links below.

Abstract

<p>In contrast to a transition system specification in process algebra, a structural operational semantics (SOS) of a programming language usually involves auxiliary entities: stores, environments, etc. When specifying SOS rules, particular auxiliary entities often need to be propagated unchan...

Full description

Published in: Electronic Notes in Theoretical Computer Science
ISSN: 1571-0661
Published: Elsevier 2009
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa25
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2013-07-23T11:49:09Z
last_indexed 2018-02-09T04:27:07Z
id cronfa25
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2013-10-17T15:27:59.2380209</datestamp><bib-version>v2</bib-version><id>25</id><entry>2012-02-23</entry><title>Implicit propagation in structural operational 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>2012-02-23</date><deptcode>FGSEN</deptcode><abstract>&lt;p&gt;In contrast to a transition system specification in process algebra, a structural operational semantics (SOS) of a programming language usually involves auxiliary entities: stores, environments, etc. When specifying SOS rules, particular auxiliary entities often need to be propagated unchanged between premises and conclusions. The standard technique is to make such propagation explicit, using variables. However, referring to all entities that need to be propagated unchanged in each rule can be tedious, and it hinders direct reuse of rules in different language descriptions.&lt;/p&gt;&lt;p&gt;This paper proposes a new interpretation of SOS rules, such that each auxiliary entity is implicitly propagated in all rules in which it is not mentioned. The main benefits include significant notational simplification of SOS rules and much-improved reusability. This new interpretation of SOS rules is based on the same foundations as Modular SOS, but avoids the notational overhead of grouping auxiliary entities together in labels.&lt;/p&gt;&lt;p&gt;After motivating and explaining implicit propagation, the paper considers the foundations of SOS and Modular SOS specifications, and defines the meaning of SOS specifications with implicit propagation by translating them to Modular SOS. It then shows how implicit propagation can simplify various rules found in the SOS literature.&lt;/p&gt;</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Electronic Notes in Theoretical Computer Science</journal><volume>229</volume><journalNumber>4</journalNumber><paginationStart>49</paginationStart><paginationEnd>66</paginationEnd><publisher>Elsevier</publisher><placeOfPublication/><issnPrint>1571-0661</issnPrint><issnElectronic/><keywords/><publishedDay>6</publishedDay><publishedMonth>8</publishedMonth><publishedYear>2009</publishedYear><publishedDate>2009-08-06</publishedDate><doi>10.1016/j.entcs.2009.07.073</doi><url/><notes>In SOS 2008, Proc. 5th Workshop on Structural Operational Semantics, Reykjavik, Iceland</notes><college>COLLEGE NANME</college><department>Science and Engineering - Faculty</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>FGSEN</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2013-10-17T15:27:59.2380209</lastEdited><Created>2012-02-23T17:02:03.0000000</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Peter</firstname><surname>Mosses</surname><orcid>0000-0002-5826-7520</orcid><order>1</order></author><author><firstname>Mark J</firstname><surname>New</surname><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2013-10-17T15:27:59.2380209 v2 25 2012-02-23 Implicit propagation in structural operational semantics 3f13b8ec315845c81d371f41e772399c 0000-0002-5826-7520 Peter Mosses Peter Mosses true false 2012-02-23 FGSEN <p>In contrast to a transition system specification in process algebra, a structural operational semantics (SOS) of a programming language usually involves auxiliary entities: stores, environments, etc. When specifying SOS rules, particular auxiliary entities often need to be propagated unchanged between premises and conclusions. The standard technique is to make such propagation explicit, using variables. However, referring to all entities that need to be propagated unchanged in each rule can be tedious, and it hinders direct reuse of rules in different language descriptions.</p><p>This paper proposes a new interpretation of SOS rules, such that each auxiliary entity is implicitly propagated in all rules in which it is not mentioned. The main benefits include significant notational simplification of SOS rules and much-improved reusability. This new interpretation of SOS rules is based on the same foundations as Modular SOS, but avoids the notational overhead of grouping auxiliary entities together in labels.</p><p>After motivating and explaining implicit propagation, the paper considers the foundations of SOS and Modular SOS specifications, and defines the meaning of SOS specifications with implicit propagation by translating them to Modular SOS. It then shows how implicit propagation can simplify various rules found in the SOS literature.</p> Conference Paper/Proceeding/Abstract Electronic Notes in Theoretical Computer Science 229 4 49 66 Elsevier 1571-0661 6 8 2009 2009-08-06 10.1016/j.entcs.2009.07.073 In SOS 2008, Proc. 5th Workshop on Structural Operational Semantics, Reykjavik, Iceland COLLEGE NANME Science and Engineering - Faculty COLLEGE CODE FGSEN Swansea University 2013-10-17T15:27:59.2380209 2012-02-23T17:02:03.0000000 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Peter Mosses 0000-0002-5826-7520 1 Mark J New 2
title Implicit propagation in structural operational semantics
spellingShingle Implicit propagation in structural operational semantics
Peter Mosses
title_short Implicit propagation in structural operational semantics
title_full Implicit propagation in structural operational semantics
title_fullStr Implicit propagation in structural operational semantics
title_full_unstemmed Implicit propagation in structural operational semantics
title_sort Implicit propagation in structural operational semantics
author_id_str_mv 3f13b8ec315845c81d371f41e772399c
author_id_fullname_str_mv 3f13b8ec315845c81d371f41e772399c_***_Peter Mosses
author Peter Mosses
author2 Peter Mosses
Mark J New
format Conference Paper/Proceeding/Abstract
container_title Electronic Notes in Theoretical Computer Science
container_volume 229
container_issue 4
container_start_page 49
publishDate 2009
institution Swansea University
issn 1571-0661
doi_str_mv 10.1016/j.entcs.2009.07.073
publisher Elsevier
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
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 0
active_str 0
description <p>In contrast to a transition system specification in process algebra, a structural operational semantics (SOS) of a programming language usually involves auxiliary entities: stores, environments, etc. When specifying SOS rules, particular auxiliary entities often need to be propagated unchanged between premises and conclusions. The standard technique is to make such propagation explicit, using variables. However, referring to all entities that need to be propagated unchanged in each rule can be tedious, and it hinders direct reuse of rules in different language descriptions.</p><p>This paper proposes a new interpretation of SOS rules, such that each auxiliary entity is implicitly propagated in all rules in which it is not mentioned. The main benefits include significant notational simplification of SOS rules and much-improved reusability. This new interpretation of SOS rules is based on the same foundations as Modular SOS, but avoids the notational overhead of grouping auxiliary entities together in labels.</p><p>After motivating and explaining implicit propagation, the paper considers the foundations of SOS and Modular SOS specifications, and defines the meaning of SOS specifications with implicit propagation by translating them to Modular SOS. It then shows how implicit propagation can simplify various rules found in the SOS literature.</p>
published_date 2009-08-06T03:05:38Z
_version_ 1756686857651879936
score 10.927057