¡Nieve en Buenos Aires! Tenía que decirlo, bueno, ahora lo "importante":
Durante el finde largo y las últimas horas de este martes que se va programé la verificación en tiempo de ejecución de los predicados tales como invariantes, precondiciones, etc. Falta verificar que los variantes decrecen.
De todas formas eso no es más que un pasatiempo para demorar las decisiones que tarde o temprano va a haber que tomar.
Por un lado quiero darle una segunda oportunidad a Simplify, un demostrador desarrollado por Compaq (cuando todavía existía) y que a Dani en un primer momento no le cerró, pero vi un par de personas que lo usan para cosas con cuantificadores (¡muchos cuantificadores!) y quiero ver cómo se comporta.
Por otro lado está la idea de usar mútiples demostradores en paralelo y ver cuál demuestra primero, de esta forma se aprovechan los puntos fuertes de cada uno.
Está también la idea, que debería empezar a delinear, de realizar ejecución simbólica de instrucciones sobre un dominio abstracto abstracto (sí, repetí abstracto).
Por último a mi me gustaría decidir cómo incorporar los arreglos. Una forma es dando un soporte genérico (instrucciones de store y load). Otra forma es dar una única operación sobre la cual podamos controlar un poco más, aunque no me queda muy claro cómo.
Ah, además Diego insiste (y con razón) en que lea un poco más, cosa que quiero hacer, pero una vez que haya decidido (más o menos) para donde encarar.
Durante el finde largo y las últimas horas de este martes que se va programé la verificación en tiempo de ejecución de los predicados tales como invariantes, precondiciones, etc. Falta verificar que los variantes decrecen.
De todas formas eso no es más que un pasatiempo para demorar las decisiones que tarde o temprano va a haber que tomar.
Por un lado quiero darle una segunda oportunidad a Simplify, un demostrador desarrollado por Compaq (cuando todavía existía) y que a Dani en un primer momento no le cerró, pero vi un par de personas que lo usan para cosas con cuantificadores (¡muchos cuantificadores!) y quiero ver cómo se comporta.
Por otro lado está la idea de usar mútiples demostradores en paralelo y ver cuál demuestra primero, de esta forma se aprovechan los puntos fuertes de cada uno.
Está también la idea, que debería empezar a delinear, de realizar ejecución simbólica de instrucciones sobre un dominio abstracto abstracto (sí, repetí abstracto).
Por último a mi me gustaría decidir cómo incorporar los arreglos. Una forma es dando un soporte genérico (instrucciones de store y load). Otra forma es dar una única operación sobre la cual podamos controlar un poco más, aunque no me queda muy claro cómo.
Ah, además Diego insiste (y con razón) en que lea un poco más, cosa que quiero hacer, pero una vez que haya decidido (más o menos) para donde encarar.
No hay comentarios.:
Publicar un comentario