PDF de programación - Formalización de la semántica del lenguaje de programación Lua

Formalizaci´on de la sem´antica del lenguaje

de programaci´on Lua

Tesista: Mallku Ernesto Soldevila Raffa.

Director: Dr. Daniel Lima Ventura.

Formalizaci´on de la sem´antica del lenguaje de programaci´on Lua. Por Mallku Ernesto Soldevila Raffa.
Se distribuye bajo una Licencia Creative Commons Atribuci´on 2.5 Argentina

1

´Indice

1 Resumen

2 Abstract

3 Introducci´on al presente trabajo

3.1.1

3.1 Motivaci´on . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Sobre Lua . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . .
3.2 Formalizaci´on y trabajos relacionados
3.3 Propuesta de trabajo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.4 Sobre sem´antica de reducciones y su mecanizaci´on con PLT Redex . . . . . . . . .

4 Presentaci´on del lenguaje n´ucleo de Lua

4.1 Tipos
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2 Estado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2.1 Valores de tipo referencia . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2.2 Tablas mutables
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2.3 Entorno . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2.4 Almacenamiento . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.3 Manejo de errores . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.4 Mecanismo de meta-tablas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.5 Recolecci´on de basura . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.6 Construcciones presentes en nuestro lenguaje . . . . . . . . . . . . . . . . . . . . .

5 Gram´atica del lenguaje n´ucleo

. . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.1 Gram´atica de programas v´alidos
5.2 Extensiones de la gram´atica . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.2.1 Nuevas categor´ıas sint´acticas
. . . . . . . . . . . . . . . . . . . . . . . . . .
5.2.2 Contextos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

6 Sem´antica de reducciones

6.1 Manipulaci´on de almacenamientos
. . . . . . . . . . . . . . . . . . . . . . . . . . .
6.2 Manipulaci´on de entornos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.3 Dise˜no de las nociones de reducci´on . . . . . . . . . . . . . . . . . . . . . . . . . .
6.4 Sem´antica de expresiones
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.4.1 Expresiones que no interact´uan con contextos . . . . . . . . . . . . . . . . .
6.4.2 Expresiones que interact´uan con el almacenamiento de valores simples . . .
6.4.3 Expresiones que interact´uan con el almacenamiento de objetos
. . . . . . .
6.4.4 Expresiones que interact´uan con ambos almacenamientos
. . . . . . . . . .
6.4.5 Mecanismo de meta-tablas . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.5 Sentencias . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . .
Sentencias que no interact´uan con almacenamientos
6.5.1
. . . . . . . . . . . . . . . .
Sentencias que operan sobre el contexto actual
6.5.2
Sentencias que no operan con almacenamientos, ni descartan el contexto . .
6.5.3
Sentencias que interact´uan con el almacenamiento de valores simples . . . .
6.5.4
6.5.5
Sentencias que interact´uan con el almacenamiento de objetos . . . . . . . .
6.5.6 Mecanismo de meta-tablas . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.6 Relaci´on de reducci´on est´andar . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

2

4

5

6
6
6
9
9
9

12
12
12
13
14
14
15
15
16
16
16

17
17
19
20
21

24
24
25
27
28
28
38
38
45
47
52
52
52
54
56
57
58
59

7 Compilaci´on de un programa en Lua

7.1 Entornos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.2 Traducci´on c´odigo fuente a c´odigo fuente . . . . . . . . . . . . . . . . . . . . . . . .

8 Entorno de ejecuci´on

8.1 Procedimientos de envoltorio . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
8.2 Servicios descritos como implementaciones en nuestro lenguaje
. . . . . . . . . . .
ipairs
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
pairs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
tostring . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Servicios que . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

8.2.1
8.2.2
8.2.3
8.2.4

9 Mecanizaci´on con PLT Redex

9.1 Gram´atica . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
9.2 Meta-funciones . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
9.3 Nociones de reducci´on . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
9.4 Verificaci´on de la sem´antica . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

61
61
62

67
67
68
68
69
70
71

73
73
73
74
74

3

1

Resumen

Los lenguajes de “script” cumplen hoy un papel importante en el desarrollo de aplicaciones, ofre-
ciendo conceptos para la programaci´on, que pueden extender aquellos presentes en el lenguaje
empleado para implementar la arquitectura de una aplicaci´on. En ese sentido, Lua es un lenguaje
pensado para ser utilizado como una herramienta para la programaci´on, de prop´osito espec´ıfico,
para implementar c´odigo a ejecutarse embebido en una aplicaci´on anfitri´on. Presenta conceptos
´utiles para el desarrollo ´agil de c´odigo, como tipado din´amico y gesti´on autom´atica de memoria,
como tambi´en mecanismos de reflexi´on, que permiten adaptarlo a dominios espec´ıficos.

Actualmente, existe un inter´es en disponer de un modelo formal del lenguaje, que permita el de-
sarrollo de herramientas para verificar propiedades sobre programas escritos en Lua. En el presente
trabajo, proponemos una sem´antica operacional para un subconjunto de los conceptos del lenguaje
Lua y los servicios ofrecidos por su librer´ıa est´andar. A su vez, empleando la herramienta PLT
Redex, realizamos una transcripci´on del modelo obtenido y efectuamos pruebas de conformidad
del mismo con respecto al int´erprete de Lua, versi´on 5.2, empleando su propia suite de pruebas.

4

2

Abstract

Script languages have an important role today in the development of applications, offering concepts
for programming, that can extend those present in the language used for the implementation of
the application’s architecture. In that matter, Lua is a language developed to be used as a tool for
programming code of special purpose, to be executed embedded into a host application. It presents
concepts that are useful for agile development of code, as dynamic typing and automatic memory
management, and also reflection mechanisms, that bring the possibility of adapt the language to
specific domains.

Currently, there is interest in having a formal model of the language, that allows the develop-
ment of tools for verification of properties of programs written in Lua. In the present work, we
propose an operational semantics for a subset of the concepts of Lua and the services offered by
its standard library. Also, using the tool PLT Redex, we transcribe the obtained model and run
tests of conformity of it, against Lua’s interpreter, version 5.2, using its own test suite.

5

3

Introducci´on al presente trabajo

3.1 Motivaci´on

Los lenguajes de “script” cumplen hoy un papel importante en el desarrollo de aplicaciones, intro-
duciendo elementos din´amicos y siendo utilizados en la orquestaci´on de las funcionalidades de tales
aplicaciones. Lua es un lenguaje que se viene destacando en este sentido debido a la posibilidad
que ofrece de extender y modificar su sem´antica, como tambi´en a lo compacto que es el lenguaje.
En este trabajo deseamos formalizar y estudiar una sem´antica operacional para el lenguaje.

Para los lenguajes de programaci´on, una formalizaci´on de su sem´antica puede ser empleada
para garantizar que una implementaci´on coincida con una especificaci´on. Por ejemplo, proyectos
como Compcert1 y Concurrent C Minor Project2 en donde se realizan verificaciones formales de
compiladores reales, trabajando sobre la definici´on de la sem´antica del lenguaje fuente (lenguaje
para el cual se construye el compilador), el intermediario (empleando internamente en el proceso
de compilaci´on) y el lenguaje objetivo (lenguaje hacia el cual se compila el programa en el lenguaje
fuente).

3.1.1 Sobre Lua

Lua es un lenguaje de script desarrollado con el objetivo de ser extensible y que sirva como lenguaje
de extensi´on [13]. El lenguaje fue pensado para ser compacto, con mecanismos que faciliten su uso
con C y que pueda ser f´acilmente embebido en las aplicaciones [14]. Lua es un lenguaje de extensi´on
en el sentido de que va a proveer caracter´ısticas como tipos din´amicos e mecanismos de reflexi´on
que pueden ser utilizados para facilitar la programaci´on de una aplicaci´on. La habilidad de Lua de
ser extensible significa que posee una serie de mecanismos que permiten modificar la sem´antica de
algunas operaciones, para adaptar el lenguaje a distintos paradigmas de programaci´on. A trav´es
del mecanismo provisto por las metatablas, las cuales definen el comportamiento de las operaciones
que es posible de realizar sobre valores de cualquier tipo, es posible modelar otros paradigmas de
programaci´on.

Como ejemplo de las posibilidades que ofrece Lua para ser adaptado a dominios espec´ıficos, y a
modo de introducci´on de la sint´axis y las posibilidades del lenguaje, veamos c´omo es posible emplear
el mecanismo de metatablas, junto a las tablas de Lua, para implementar la noci´on de clases e
instancias, del paradigma orientado a objetos3. El empleo de tablas para representar objetos y
clases resulta posible gracias a que todos l