search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
240 stars 33 forks source link

Implement `sAssert` #94

Closed LeventErkok closed 9 years ago

LeventErkok commented 10 years ago

We want to be able to say:

sAssert (b /= 0) "Safety: division by 0" (a / b)

and have SBV spit out a model right then and there during symbolic simulation if the condition is not necessarily true, similar to sBranch.

This shouldn't be hard to implement; though not clear if SBV should throw an error, or should return something back to the user. Former would be easy to implement, latter might be better for people building libraries on top of SBV.

LeventErkok commented 9 years ago

The easiest thing to do here is to throw an error. In fact, it's not even clear how to pass this back up to the user, as we'd need to lift this up from an expression to a Symbolic-level thing, which is just the wrong thing to do. This is the EDSL conundrum: The fact remains that we have "pure" looking expressions and we've to obey. Sigh.. So, "error" it is. Implementation coming shortly.