Me he interesado y estoy buscando ejemplos prácticos del uso de SMT Z3 (como DbC) con código y alternativas de código abierto para esta herramienta. Así que, de hecho, estoy interesado en las herramientas de resolución formales similares Z3, pero:¿Está buscando ejemplos prácticos de cajas de uso SMT Z3 (como DbC) y alternativas de código abierto a Z3?
- que debe ser de código abierto
- proporcionar tanto de bajo nivel (API) y el alto nivel (scripting texto) la interacción
- soporte SMT-LIB
- adecuada (utilizable) en herramientas/escritos en/para lenguajes como Java, Python, ruby, Vala, y no Haskell
- tiene herramientas estables (utilizables en la práctica) sobre la base de que, como diseño por contrato (DbC), verificación de tipo estático, etc.
De acuerdo a la página principal SMT-LIB (véase bit.ly paquete para más detalles) la lista de solucionadores de 2010 SMT es: "Alt-Ergo, Barcelogic, Beaver, Boolector, CVC3, DPT, MathSAT, OpenSMT, satén, Spear, STP, SWORD, UCLID, veriT, Yices, Z3. "
Por favor, dar su opinión sobre el uso de cualquiera de ellos en la práctica (ejemplos de código son los mejores)?
Finalmente, cualquier información sobre la comparación con las posibilidades de GHC sería útil, pero solo en caso de que exista un ejemplo de implementación (no una "característica" de idioma).
Más información rápida sobre Z3 aquí http://bit.ly/bundles/ewiger/1