Avanzo en mi TODO list

De mi lista del post anterior pude implementar hablar con provers de primer orden y verificar accesos a arreglos son en rango.

Mañana tenemos con Diego y Dani una reunión donde definir un poco mejor cómo seguimos, de todas formas algunas cosas que quiero hacer en estos días son:

• cambiar la estructura de iteración
  
• inferir postcondiciones
• procedimientos
• plugin de eclipse, basado en el código fuente del plugin de javaCC

Una buena nueva es que pude demostrar la corrección de bubblesort, antes no podía porque un invariante tenía un error. Y ahora estoy tratando de demostrar el hecho de que el arreglo es permutación del original (asumiendo que no hay repetidos).