[Haskell-cafe] ANN improve-0.0.4
Tom Hawkins
tomahawkins at gmail.com
Wed Aug 11 13:00:16 EDT 2010
Hi,
ImProve [1] is a little imperative DSL that compiles to C code.
Intended for high assurance embedded applications, ImProve is also an
infinite state, unbounded model checker. Meaning ImProve can verify
assertions in a program will always be true. Here's an example:
module Main where
import Language.ImProve
launchControl :: Stmt ()
launchControl = do
presidentialAuthority <- input bool "presidentialAuthority"
buttonPressed <- input bool "buttonPressed"
launchMissiles <- bool' "launchMissiles" $
(presidentialAuthority ||. buttonPressed)
assert "conditionsToLaunch" $ launchMissiles ==.
(presidentialAuthority &&. buttonPressed)
main :: IO ()
main = verify "yices" 20 launchControl
Running this program yields:
verifying conditionsToLaunch FAILED: disproved basis in k = 1 (see trace)
On verification failures, ImProve will emit a counter example showing
the violation, which is essentially a program trace showing how things
could go wrong. In this case, the trace looks like this:
initialize launchMissiles := false
cycle 0
input presidentialAuthority <== true
input buttonPressed <== false
launchMissiles <== true
assertion FAILED: conditionsToLaunch
This basically means Barack was somehow able to launch on his own.
(Man! I even voted for the guy!)
Under the hood, ImProve uses Yices [2] for SMT solving, and a method
of unbounded model checking known as k-induction.
Don't expect too much from ImProve; it's a very restrictive language.
It's basically three data types (bool, int, float), variables
assignments, and 'if' statements. No procedures, no loops, no arrays,
no pointers, etc. However, it can still do interesting things --
especially with Haskell combinators in play.
Hope you find it useful. And as always, questions, comments, and
feedback welcome.
-Tom
[1] http://hackage.haskell.org/package/improve
[2] http://yices.csl.sri.com/
More information about the Haskell-Cafe
mailing list