Arreglo todo, rompo todo, arreglo todo...

Ayer y hoy me dediqué a cambiar el lenguaje para incorporarle los scopes. Primero que nada tuve que cambiar la symbol table para que pueda trabajarse con distintas encarnaciones de un mismo nombre, y ahora estoy trabajando sobre los nombres de estados y otras yerbas.

Pero no todo es romper, ¡el otro día antes de cambiar el lenguaje pude demostrar la corrección de un programa que calcula la suma de los primeros n naturales! :)

¡Muy, muy contento!

Así es como me siento en este momento de la noche, en un día lleno de PROblemas políticos que se vienen en el horizonte.

Y no me siento culpable por sentirme así, ya que la causa de esta alegría es que encontré programando una forma de no pensar en lo nefasto de la situación que se viene...

En concreto, implementé soporte para loops y de esa manera el lenguaje sobre el que corro las verificaciones se volvió infinitamente más expresivo.

Ya demostré la corrección de un programa que calcula la copia de un número mediante incrementos de a uno y un programa que calcula el cociente y el resto de una división.

En estos días voy a ver de terminar de entender y luego implementar una forma de tratar scoping y generalizar el concepto de pre y post condiciones que se le ocurrió a Dani.

Una tarde charlando...

... en el comedor de la facu.

Repasamos junto con Dani y Diego los avances que hubo en la implementación que estuve haciendo y brevemente cómo seguir.

Por un lado quiero completar la posibilidad de analizar programas con ciclos, con la versión del lenguaje tal como está y a eso me voy a dedicar en el futuro inmediato.

Pero por otra parte el lenguaje está empezando a mostrar las primeras señales de que si no lo definimos formalmente nos va a estallar en la cara en el momento menos deseado.

Así que de acá a un tiempo no muy lejano la idea es definir lo mejor posible tanto el lenguaje intermedio como el de alto nivel (o al menos algunos lineamientos).

Hay que decidir cuestiones como:

• de qué forma se trabajará la semántica de parámetros,
  
• qué cosas se asumen como obvias en las post-condiciones (e invariantes) y no son necesarias decir (a = a@pre, b = b@pre, etc...),
• si el lenguaje de alto nivel se traducirá de forma sencilla o también este pasaje al intermedio requiere de análisis "semánticos" y validación de algunas cuestiones usando el demostrador.
• ¡un nombre por favor para el lenguaje alto y el intermedio así podemos hablar entre nosotros y saber a qué nos referimos!

¡Muy contento!

Después de algunos días construyendo un parser y definiendo una sintáxis abstracta, empecé a definir la semántica a través de traducciones a lógica.

Todavía no soporto ciclos, pero hace apenas 5 minutos pude demostrar la correctitud del siguiente programa, muy básico, pero algo al fin...

f(in a, out b)
:? a != 0
:! b > 10
{
____b <- 0
____c <- not a
____if a then {
________if c then {
________} else {
____________b <- b + 5
________}
________b <- b + 5
____} else {
________b <- b + 1
____}
____b <- b + 1
}

Idea

Tengo la impresión de que el lenguaje de especificación permite expresar formulas demasiado complejas (con varios niveles de anidamiento, etc.). Esto puede que perjudique el funcionamiento del demostrador.

Probar reduciendo la complejidad de las fórmulas al permitir únicamente comparar variables. Cualquier cosa más compleja deberá ser simulada creando variables y hacerlas valer lo que uno quiere comparar a través de instrucciones del lenguaje de programación.

Manos a la obra...

Charlamos con Dani y Diego. El objetivo a corto plazo es tener un lenguaje monoprocedural con enteros y arreglos. Este lenguaje le exige al programador que escriba una pre y una post condición las cuales pueden incluir cuantificadores acotados. Los ciclos deben incluir invariante y función variante.

Una vez definido la idea es basarme en una herramienta proof of concept de Dani para generar aserciones y consultas en un demostrador de teoremas que permitirá (si todo sale bien) demostrar la corrección del programa.

También estuvimos pensando en definir un segundo lenguaje, de nivel más alto que el primero donde ciertas construcciones modelen tipos de iteración comunes, para de esta forma tener ciertos invariantes precalculados. Supongo que esto lo veremos una vez que esté bien definido el lenguaje mencionado más arriba (que por ahora llamaré "lenguaje intermedio").

¿Quizás un rumbo nuevo?

Estuvimos charlando con Diego G. y Daniel G. porque existía la posibilidad de tomar un rumbo relativamente distinto en la tesis.

Dani propone analizar un lenguajecito muy chico, inventado por nosotros para demostrar que el código cumple con la especificación, suponiendo que el usuario provee precondición, postcondición e invariantes para los ciclos.

Si logramos hacer inferencia de invariantes con una herramienta similar a la de Diego P., luego la usabilidad sería relativamente alta y el lenguajecito podría ir creciendo hasta tener algo relativamente serio.

Veremos cómo sigue esto, es una opción más que interesante.

¡Y hoy paso el tiempo...

... resumiendo papers!

http://docs.google.com/Doc?id=dt3n7b3_5gmsg74