jueves, 9 de agosto de 2007

Inferencia de postcondiciones

Hoy implementé una versión básica de inferencia de postcondiciones. Esto es necesario para poder contar con estructuras de iteración relativamente piolas como por ejemplo la asignación simultánea. Todavía hay varias cosas que pulir.

También estoy cada vez más seguro de que necesito una capa extra de abstracción entre los predicados que utilizo y los provers. Esto puede ser un poco denso de implementar pero hay varios indicios que marcan que sería el camino correcto a seguir, aunque por ahora (mientras no me trabe) es algo que voy a patear...

No hay comentarios.: