(Copiado de un mail a mis directores)
Las buenas:
- Ahora PEST tiene "For" (for var from low to high do {...}) que no necesitan de proveer invariante y tampoco variante.
- Me maté programando y cambie casi toda la estructura que usaba para almacenar las VC's. ahora se hace en dos pasadas:
1) se recorre el programa PEST de arriba hacia abajo haciendo dynamic single assignment. Se obtiene algo que llamo "lenguaje intermedio" que sería similar a boogie: tiene assume, assert, if, lemma (para simular el assume false de boogie).
El lenguaje intermedio también tiene una construccion especial llamada "For" que, como su nombre lo indica, representa de forma temporaria los For's no resueltos del lenguaje Pest. o sea, durante la primera pasada no se generan VC's para la correctitud del For, solamente se generan para la correctitud de su cuerpo (recursivamente).
2) Se recorre el lenguaje intermedio de ABAJO hacia arriba para remover los For's no resueltos. Esto permite que en cada paso ya tener la cola resuelta, es decir con todos sus For's reemplazados por lemmas que deberían probar que son correctos.
En cada paso que se encuentra un For se calcula la wp de la cola (que como no tiene for's, se puede obtener tranquilamente). Se la debilita y se usa eso como invariante. Es decir: se pregunta si vale antes de entrar, si se preserva y se asume al final, una vez terminado el for.
Una vez eliminado el For, se reemplaza por un lema muy similar a lo que hubiera quedado si en vez de un For era un While común (con invariante, etc.). La diferencia es que no es necesario ver la terminación, está garantizada por la estructura misma.
- Esto lo probé únicamente en el caso para calcular el máximo de un arreglo y parece funcionar. Pero quiero probarlo en casos donde haya código entre el fin del for y el fin del procedimiento, de manera tal de tener que calcular una wp más compleja que simplemente la postcondicion del procedimiento.
- Otros cambios pequeños: ahora PEST tiene como nativos comandos assume y assert. yo no los dejaría en el lenguaje final, pero para testear cosas son útiles. esta caracteristica, junto con los procedimientos hizo que los bloques con pre y post sean obsoletos, así que los saqué.
Las malas:
Al cambiar la estructura necesité retocar bastante fuertemente la forma en la que trabajo con predicados internamente. Para calcular wp's necesito a veces cuantificar arreglos y ahora los arreglos son ciudadanos de primer nivel en los predicados. Es decir un store sobre un arreglo es un término. Y todo eso los provers de primer orden no lo soportan así que temporariamente los desconecté.
Se me ocurre que con algún tipo de preproceso a los predicados se pueden eliminar las cuantificaciones de arreglos (esto no se puede hacer en el caso general, pero la pinta de las cuantificaciones que aparecen parecería ser simple). Y cambiar los update terms por renombres y axiomas que digan como se relacionan.
Pero considerando que los provers de primer orden no habían aportado nada (o sea, no encontré ningún caso donde puedan probar algo que los SMT solvers no pudieran, sino más bien todo lo contrario) por ahora no quiero invertir tiempo en hacer toda esta traducción que parece ser nada trivial.
Pero por ahora me parece más interesante ver qué potencia y limitaciones tiene nuestro brand-new For y el cálculo de wp's.
