Zainteresowałem się i szukałem praktycznych przykładów użycia SMT Z3 (np. DbC) z kodem i alternatywami open source do tego narzędzia. Tak, w istocie, jestem zainteresowany w podobnych Z3 narzędzi formalny rozwiązywania, ale:Szukasz praktycznych przykładów zastosowań SMT Z3 (jak DbC) i alternatywy open source dla Z3?
- musi być open source
- zapewniają zarówno niskiego poziomu (API) oraz wysokiego poziomu (skryptowy Text) interakcji
- wsparcie SMT-LIB
- nadaje (użytkowej) w narzędzia/zapisywane w/w języków jak Java, Python, Ruby, Vala i nie Haskell
- ma stabilne (użyteczne w praktyce) narzędzia oparte na nim, jak projektowanie według umowy (DbC), statyczna weryfikacja typu itp.
Według SMT-lib głównej (patrz bit.ly pakiet szczegóły) lista 2010 SMT rozwiązują jest: „Alt-Ergo, Barcelogic, Beaver, Boolector, CVC3, DPT, MathSAT, OpenSMT, satyna, Włócznia, STP, SWORD, UCLID, veriT, Yices, Z3. "
Proszę podać informacje zwrotne na temat korzystania z nich w praktyce (przykłady kodów są najlepsze)?
Wreszcie, wszelkie informacje na temat porównania go z możliwościami GHC byłyby użyteczne, ale tylko w przypadku, gdy istnieje przykład wdrożenia (a nie "funkcja" języka).
Więcej szybka informacja na Z3 tutaj http://bit.ly/bundles/ewiger/1