PPL y preparando una charla

Estuve perdiendo bastante tiempo compilando una biblioteca o librería (como quieran llamarla) para manejar polihedros llamada PPL (Parma Polyhedra Library). Por suerte una vez concluido todo el asunto con éxito, pude engancharla con Java y ejecutar un pequeño test. Ahora debería empezar a montar una interfaz para trabajar contra esta o cualquier otra librería de polihedros.

Además estuve empezando a armar slides para dar una charla interna este jueves a la gente de la oficina. Dani y Diego me estuvieron dando una mano revisando lo que había hecho, que creo que está dentro de todo bien. Falta ampliar un poco algunas secciones y agregar algunas imágenes.

Frío, código y finde largo

¡Nieve en Buenos Aires! Tenía que decirlo, bueno, ahora lo "importante":

Durante el finde largo y las últimas horas de este martes que se va programé la verificación en tiempo de ejecución de los predicados tales como invariantes, precondiciones, etc. Falta verificar que los variantes decrecen.

De todas formas eso no es más que un pasatiempo para demorar las decisiones que tarde o temprano va a haber que tomar.

Por un lado quiero darle una segunda oportunidad a Simplify, un demostrador desarrollado por Compaq (cuando todavía existía) y que a Dani en un primer momento no le cerró, pero vi un par de personas que lo usan para cosas con cuantificadores (¡muchos cuantificadores!) y quiero ver cómo se comporta.

Por otro lado está la idea de usar mútiples demostradores en paralelo y ver cuál demuestra primero, de esta forma se aprovechan los puntos fuertes de cada uno.

Está también la idea, que debería empezar a delinear, de realizar ejecución simbólica de instrucciones sobre un dominio abstracto abstracto (sí, repetí abstracto).

Por último a mi me gustaría decidir cómo incorporar los arreglos. Una forma es dando un soporte genérico (instrucciones de store y load). Otra forma es dar una única operación sobre la cual podamos controlar un poco más, aunque no me queda muy claro cómo.

Ah, además Diego insiste (y con razón) en que lea un poco más, cosa que quiero hacer, pero una vez que haya decidido (más o menos) para donde encarar.

Cerrando la semana

Estuve laburando en integrar un demostrador genérico. Para no complicarse con librerias lo hago a travez de un llamado al programa y me engancho escribiendo en su input, leyendo su output desde java, lo cual permite integracion con cualquier demostrador para el cual contemos con:

• un ejecutable
• un convertidor de mis predicados a predicados en el lenguaje del demostrador
• un intérprete para la salida del demostrador que mapee a VALID, INVALID, UNKNOWN

También estuve generando código java a partir de nuestros programas y lo que quedó funciona muy bien (¡incluso los genera sin warnings!). Lo que por ahora (por falta de tiempo) no hace es generar código (assertions) que verifiquen que las pre y post valen en tiempo de ejecución.

Por último estuve jugando con los dos demostradores (yices y cvc) para ver que tanto se bancan arrays y cuatificadores. En mi experiencia cada vez que digo algo cuantificado universalmente la respuesta es unknown. Realmente estoy empezando a dudar seriamente de que algo con arrays pueda llegar siquiera a hacerse (siempre y cuando nos quedemos en el mundo de los demostradores automáticos). En caso de que esto sea tan malo como parece, creo que vamos a necesitar un "plan b"... porque introducir arrays sería equivalente a demostrar todos los programas EXCEPTO aquellos que tienen arrays... algo bastante ridículo.

Un nuevo demostrador, velitas y desilución

El martes leyendo por ahí alguna web que ya no recuerdo, encontré un demostrador que se llama Yices, que le gana a todo el resto según los resultados de una competencia llamada SMT-COMP.

El miércoles cumplí 24 años. A pesar de que estuve en la facu un rato, mucho no laburé.

El jueves, o sea, hoy, implementé el binding necesario para utilizar este otro demostrador. Y me llevé una triste sorpresa al comprobar que no soporta bajo ningún concepto aritmética no lineal. O sea... que no me sirve para casi nada...

Sin procedimientos

Después de charlar con Diego y Dani llegamos a la conclusión de que por lo pronto iremos para adelante sin procedimientos, volviendo a la vieja idea de los bloques con pre y postcondiciones.

Hoy programé un rato y finalmente lo tengo andando: verifica loops y todo.

Además me contestó la gente de CVC3, diciendo que todavía no tuvieron tiempo de ver un bug report que les envié, pero que cualquier novedad me lo harían saber.

¿Procedimientos?

Después de varios días de reestructurar código llegué a una especie de callejón sin salida al querer implementar bloques con pre y post condiciones.

No queda claro qué cosas modifican y qué cosas no y cómo vincular esto con el resto del código que envuelve ese bloque.

Una forma posible de resolverlo es definir muy claramente cuál es la semántica con la que queremos trabajar con dichos bloques, pero creo que el problema es equivalente al de definir una semántica formal para trabajar con procedimientos.

Por lo tanto se me ocurre que es mejor optar por empezar a manejar procedimientos y matar dos pájaros de un tiro.

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! :)