Estuve aumentando el lenguaje PEST para que pueda hablar de arreglos. Además, ya que estaba tocando el parser, mejoré la sintaxis de expresiones para que se puedan escribir cosas complejas en una misma sentencia como:
x <- a[i] + 3*i
Por otra parte reimplementé el output a SMT-lib porque la traducción que ofrecía CVC era muy mala para lidiar con operadores aritméticos no lineales.
Para poder soportar aritmética no lineal en Z3 y Yices lo que hice fue crear operadores no interpretados para la suma y la división. La idea es axiomatizarlos lo más posible (sin que pinche) y demostrar algunas cosas... que siempre es mejor que nada.
Con todo esto pude demostrar la corrección de programas como el máximo de un arreglo, el arreglo 1...N, incrementar en 1 cada posición de un arreglo, ver si un arreglo está ordenado, etc.
x <- a[i] + 3*i
Por otra parte reimplementé el output a SMT-lib porque la traducción que ofrecía CVC era muy mala para lidiar con operadores aritméticos no lineales.
Para poder soportar aritmética no lineal en Z3 y Yices lo que hice fue crear operadores no interpretados para la suma y la división. La idea es axiomatizarlos lo más posible (sin que pinche) y demostrar algunas cosas... que siempre es mejor que nada.
Con todo esto pude demostrar la corrección de programas como el máximo de un arreglo, el arreglo 1...N, incrementar en 1 cada posición de un arreglo, ver si un arreglo está ordenado, etc.
No hay comentarios.:
Publicar un comentario