Mostrar el registro sencillo del ítem
dc.contributor.author
Soldevila Raffa, Mallku Ernesto
dc.contributor.author
Ziliani, Luis Francisco
dc.contributor.author
Silvestre, Bruno
dc.date.available
2024-01-04T19:42:18Z
dc.date.issued
2022-08
dc.identifier.citation
Soldevila Raffa, Mallku Ernesto; Ziliani, Luis Francisco; Silvestre, Bruno; From Specification to Testing: Semantics Engineering for Lua 5.2; Springer; Journal Of Automated Reasoning; 66; 4; 8-2022; 905-952
dc.identifier.issn
0168-7433
dc.identifier.uri
http://hdl.handle.net/11336/222479
dc.description.abstract
We provide a formal semantics for a large subset of the Lua programming language, in its version 5.2. The semantics is a major part of an ongoing effort to construct reliable tools to analyze Lua code. In this work, we present the details of several key aspects of the language, like the semantics of its only structured data-type (tables), its meta-programming mechanism (metatables), error handling, and how these mechanisms are used to define a complex dynamic semantics that must deal with several possible erroneous situations during run time, given the nature of the language. The semantics is mechanized in Redex, a DSL specially designed to specify and debug operational semantics. We validated the mechanization in two ways: first, by executing within Redex the test suite of the reference interpreter of Lua, and second, by specifying and performing random testing of its fundamental properties using the redex-check tool. Together, they evidence that our model soundly captures the semantics of the selected fragment of the language. Additionally, we address some of the performance problems that typically arise when testing a mechanization in Redex, by using a simple implementation of a reachability-based garbage collector that captures key aspects of Lua’s. By collecting syntactic garbage, we reduce the size of configurations during run time. Finally, we briefly discuss this avenue of development of our semantics, together with the implementation of a prototype tool to perform static analysis of Lua programs.
dc.format
application/pdf
dc.language.iso
eng
dc.publisher
Springer
dc.rights
info:eu-repo/semantics/openAccess
dc.rights.uri
https://creativecommons.org/licenses/by-nc-sa/2.5/ar/
dc.subject
DOMAIN SPECIFIC LANGUAGES
dc.subject
IMPERATIVE LANGUAGES
dc.subject
LUA
dc.subject
OPERATIONAL SEMANTICS
dc.subject
RANDOMIZED TESTING
dc.subject
REDUCTION SEMANTICS
dc.subject
SEMANTICS
dc.subject.classification
Ciencias de la Computación
dc.subject.classification
Ciencias de la Computación e Información
dc.subject.classification
CIENCIAS NATURALES Y EXACTAS
dc.title
From Specification to Testing: Semantics Engineering for Lua 5.2
dc.type
info:eu-repo/semantics/article
dc.type
info:ar-repo/semantics/artículo
dc.type
info:eu-repo/semantics/publishedVersion
dc.date.updated
2024-01-04T10:49:56Z
dc.journal.volume
66
dc.journal.number
4
dc.journal.pagination
905-952
dc.journal.pais
Alemania
dc.journal.ciudad
Berlin
dc.description.fil
Fil: Soldevila Raffa, Mallku Ernesto. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física. Sección Ciencias de la Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas. Centro Científico Tecnológico Conicet - Córdoba; Argentina
dc.description.fil
Fil: Ziliani, Luis Francisco. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física. Sección Ciencias de la Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas. Centro Científico Tecnológico Conicet - Córdoba; Argentina
dc.description.fil
Fil: Silvestre, Bruno. Universidade Federal de Goiás; Brasil
dc.journal.title
Journal Of Automated Reasoning
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/url/https://link.springer.com/article/10.1007/s10817-022-09638-y
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/doi/https://doi.org/10.1007/s10817-022-09638-y
Archivos asociados