A partir de lo que ví del artículo que mencionaba ayer, surgió un detalle que es no tratar más las variables dentro de estados tipo:
at(x,S0) ó at(y,S1)
Sino tratarlas con sufijos por ejemplo
x_S0 ó y_S1
De esta manera el demostrador se ahorra tener que trabajar con la función no interpreteada 'at' y posiblemente eso sea más rápido.
La contra: las aserciones descargadas al verificador son un poquito menos legibles.
at(x,S0) ó at(y,S1)
Sino tratarlas con sufijos por ejemplo
x_S0 ó y_S1
De esta manera el demostrador se ahorra tener que trabajar con la función no interpreteada 'at' y posiblemente eso sea más rápido.
La contra: las aserciones descargadas al verificador son un poquito menos legibles.
No hay comentarios.:
Publicar un comentario