Baklanova, Nadezhda
and Ricciotti, Wilmer and Smaus, Jan-Georg and Strecker, Martin
Abstracting an Operational Semantics to Finite Automata.
(2015)
In: 11th International Conference onICT in Education, Research, and Industrial Applications (ICTERI 2015), 14 May 2015 - 16 May 2015 (Lviv, Ukraine).
|
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 188kB |
Official URL: https://doi.org/10.1007/978-3-319-30246-1_7
Abstract
There is an apparent similarity between the descriptions of small-step operational semantics of imperative programs and the semantics of finite automata, so defining an abstraction mapping from semantics to automata and proving a simulation property seems to be easy. This paper aims at identifying the reasons why simple proofs break, among them artifacts in the semantics that lead to stuttering steps in the simulation. We then present a semantics based on the zipper data structure, with a direct interpretation of evaluation as navigation in the syntax tree. The abstraction function is then defined by an equivalence class construction.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Additional Information: | Thanks to Springer editor. This papers appears in Proceedings of ICTERI 2015: Information and Communication Technologies in Education, Research, and Industrial Applications ISBN 978-3-319-30245-4, part of volume 594 of the Communications in Computer and Information Science book series (CCIS) ISSN 1865-0929 The original PDF is available at: https://link.springer.com/chapter/10.1007%2F978-3-319-30246-1_7 |
| HAL Id: | hal-01782563 |
| Audience (conference): | International conference proceedings |
| Uncontrolled Keywords: | |
| Institution: | Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE) French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE) Université de Toulouse > Université Toulouse III - Paul Sabatier - UPS (FRANCE) Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE) Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE) |
| Laboratory name: | |
| Statistics: | download |
| Deposited By: | IRIT IRIT |
| Deposited On: | 30 Mar 2018 12:33 |
Repository Staff Only: item control page
