BubbleSort, TODO

Hoy programé un BubbleSort y casi casi lo verifico completo. De 38 VC's pude verificar 37.

Tengo que revisar, quizás algún invariante está un poco débil.

También tengo una pequeña lista de cosas interesantes para hacer con respecto a la implementación:

• hablar con first-order provers
  
• verificar que los accesos a arreglos siempre son correctos
• inferir postcondiciones
• inferir precondiciones (wp)
• más benchmarks
• procedimientos
• construcciones de alto nivel (foreach, acum, select, etc.)
• ¿plugin de eclipse?

Arrays

Estuve aumentando el lenguaje PEST para que pueda hablar de arreglos. Además, ya que estaba tocando el parser, mejoré la sintaxis de expresiones para que se puedan escribir cosas complejas en una misma sentencia como:

x <- a[i] + 3*i


Por otra parte reimplementé el output a SMT-lib porque la traducción que ofrecía CVC era muy mala para lidiar con operadores aritméticos no lineales.

Para poder soportar aritmética no lineal en Z3 y Yices lo que hice fue crear operadores no interpretados para la suma y la división. La idea es axiomatizarlos lo más posible (sin que pinche) y demostrar algunas cosas... que siempre es mejor que nada.

Con todo esto pude demostrar la corrección de programas como el máximo de un arreglo, el arreglo 1...N, incrementar en 1 cada posición de un arreglo, ver si un arreglo está ordenado, etc.

SMT-lib

Descubrí que el demostrador CVC viene con una característica que permite traducir a formato SMT-lib. Este es un formato que usan todos los demostradores SMT en una competencia que se hace una vez por año.

O sea, que ahora puedo escribir en SMT-lib gratis, sin esfuerzo porque el output a CVC ya lo tenía hecho.

Un tema es que varios demostradores, al leer archivos en este formato SMT-lib, sólo le dan bola a la primer propiedad que aparece ahí. Por eso ahora lo que hago es:

1. Ir acumulando las cosas que sé que son verdad (precondición y los asserts que surgen del flujo del programa).
2. Cuando encuentro un query lo parto en tantos átomos como elementos de la conjunción que denota.
3. Para cada átomo genero un archivo con todos los asserts acumulados como axiomas y pregunto si es teorema.
   
4. Si es teorema lo agrego al conjunto de axiomas. Sino, no.
5. Sigo hasta agotar todos los átomos de cada uno de los queries.

Al finalizar eventualmente hay algunas subfórmulas que no pudieron ser probadas.

Varios días pasaron

El jueves pasado di la charla sobre lo que estuve haciendo y en términos generales gustó. Hubo muchas preguntas (tal como esperábamos) sobre para qué sirve lo que estamos haciendo y cuál es la innovación, cuestiones que ni nosotros (Dani, Diego y yo) sabemos por ahora.

Estos días estuve yendo y viniendo con refactors al código hasta que me cansé y decidí que así como está es un código suficientemente malo y suficientemente bueno.

También estuve cursando una ECI con Shaz Qadeer, la verdad me está sirviendo muchísimo para aprender cosas nuevas y profundizar y entender otras que más o menos había visto en papers.

Le mostramos a Shaz lo que tenemos hecho y le pareció bien. Le pareció que la idea de Dani de hablar con demostradores de FOL es interesante, y vale la pena probar. Por eso estos días quiero ver de hacer algunos ejemplos, aunque sea a mano.

Para piter que lo mira por tevé

Se que piter cada tanto lee este blog. Piter, comprá la licuadora que debés.

Sin 'at'

A partir de lo que ví del artículo que mencionaba ayer, surgió un detalle que es no tratar más las variables dentro de estados tipo:

at(x,S0) ó at(y,S1)

Sino tratarlas con sufijos por ejemplo

x_S0 ó y_S1

De esta manera el demostrador se ahorra tener que trabajar con la función no interpreteada 'at' y posiblemente eso sea más rápido.

La contra: las aserciones descargadas al verificador son un poquito menos legibles.

Slides listas, PPL promete, un artículo

Por partes:

• Las slides para la charla de este jueves ya están cocinadas. Puede faltar pulir un poco, pero la base está.

• Estuve jugando con la interfaz para Java de la PPL. Probé BDDs y Poliedros (el otro día me di cuenta que en castellano van sin 'h'). Aparentemente la interfaz Java no tiene bindings para trabajar con Octágonos, incluso cuando éstos están implementados en la versión 0.10pre7 (que es la que obtuve del CVS). En estos días voy a ver si hago una interfaz propia para manejar de forma más o menos cómoda la interfaz de Java de la PPL. (Y también ver de que cuando le agreguen el soporte para Octágonos a la API de Java, poder incluirlo rápidamente en mi wrapper.)

• Estuve leyendo un artículo que promete ser interesante. Menciona una combinación entre SMT solvers e interpretación abstracta. La idea es discutir este artículo con Dani y Diego para ver qué se puede aprovechar de ahí.