Hoy programé un BubbleSort y casi casi lo verifico completo. De 38 VC's pude verificar 37.
Tengo que revisar, quizás algún invariante está un poco débil.
También tengo una pequeña lista de cosas interesantes para hacer con respecto a la implementación:
Tengo que revisar, quizás algún invariante está un poco débil.
También tengo una pequeña lista de cosas interesantes para hacer con respecto a la implementación:
- hablar con first-order provers
- verificar que los accesos a arreglos siempre son correctos
- inferir postcondiciones
- inferir precondiciones (wp)
- más benchmarks
- procedimientos
- construcciones de alto nivel (foreach, acum, select, etc.)
- ¿plugin de eclipse?
1 comentario:
Una cosa interesante a explorar es random interpretation que es una suerte de combinacion forward y backward.
Publicar un comentario