Integrated operational semantics: small-step, big-step and multi-step

Hayes, Ian J. and Colvin, Robert J. (2012). Integrated operational semantics: small-step, big-step and multi-step. In: John Derrick, John Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves and Elvinia Riccobene, Abstract State Machines, Alloy, B, VDM, and Z: Third International Conference, ABZ 2012, Proceedings. 3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z (ABZ 2012), Pisa, Italy, (21-35). 18-21 June 2012. doi:10.1007/978-3-642-30885-7_2


Author Hayes, Ian J.
Colvin, Robert J.
Title of paper Integrated operational semantics: small-step, big-step and multi-step
Conference name 3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z (ABZ 2012)
Conference location Pisa, Italy
Conference dates 18-21 June 2012
Proceedings title Abstract State Machines, Alloy, B, VDM, and Z: Third International Conference, ABZ 2012, Proceedings   Check publisher's open access policy
Journal name Lecture Notes in Computer Science   Check publisher's open access policy
Place of Publication Heidelberg, Germany
Publisher Springer
Publication Year 2012
Sub-type Fully published paper
DOI 10.1007/978-3-642-30885-7_2
Open Access Status
ISBN 9783642308840
ISSN 0302-9743
1611-3349
Editor John Derrick
John Fitzgerald
Stefania Gnesi
Sarfraz Khurshid
Michael Leuschel
Steve Reeves
Elvinia Riccobene
Volume 7316
Start page 21
End page 35
Total pages 15
Collection year 2013
Language eng
Formatted Abstract/Summary
Plotkin’s structural operational semantics provides a tried and tested method for defining the semantics of a programming language via sets of rules that define valid transitions between program configurations. Mosses’ modular structural operational semantics (MSOS) recasts the approach by making use of rules consisting of labelled transitions, allowing a more modular approach to defining language semantics. MSOS can be adapted by using “syntactic” labels that allow local variables and aliasing to be defined without augmenting the semantics with environments and locations. The syntactic labels allow both state-based constructs of imperative languages and event-based constructs of process algebras to the specified in an integrated manner.
To illustrate the integrated approach we compare its rules with Plotkin’s original rules for both small-step and big-step operational semantics. One issue that arises is that defining concurrency requires the use of a small-step approach to handle interleaving, while defining a specification command requires a big-step approach. The integrated approach can be generalised to use a sequence of (small) steps as a label; we call this a multi-step operational semantics. This approach allows both concurrency and non-atomic specification commands to be defined.
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ

 
Versions
Version Filter Type
Citation counts: Scopus Citation Count Cited 1 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Mon, 24 Sep 2012, 13:13:54 EST by Ms Imogen Ferrier on behalf of School of Information Technol and Elec Engineering