Charlamos con Dani y Diego. El objetivo a corto plazo es tener un lenguaje monoprocedural con enteros y arreglos. Este lenguaje le exige al programador que escriba una pre y una post condición las cuales pueden incluir cuantificadores acotados. Los ciclos deben incluir invariante y función variante.
Una vez definido la idea es basarme en una herramienta proof of concept de Dani para generar aserciones y consultas en un demostrador de teoremas que permitirá (si todo sale bien) demostrar la corrección del programa.
También estuvimos pensando en definir un segundo lenguaje, de nivel más alto que el primero donde ciertas construcciones modelen tipos de iteración comunes, para de esta forma tener ciertos invariantes precalculados. Supongo que esto lo veremos una vez que esté bien definido el lenguaje mencionado más arriba (que por ahora llamaré "lenguaje intermedio").
Una vez definido la idea es basarme en una herramienta proof of concept de Dani para generar aserciones y consultas en un demostrador de teoremas que permitirá (si todo sale bien) demostrar la corrección del programa.
También estuvimos pensando en definir un segundo lenguaje, de nivel más alto que el primero donde ciertas construcciones modelen tipos de iteración comunes, para de esta forma tener ciertos invariantes precalculados. Supongo que esto lo veremos una vez que esté bien definido el lenguaje mencionado más arriba (que por ahora llamaré "lenguaje intermedio").
No hay comentarios.:
Publicar un comentario