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
242 stars 34 forks source link

Question: WP: `BadPrecondition` "can only happen in traceExecution" #724

Closed ocramz closed 2 months ago

ocramz commented 2 months ago

I'm struggling to understand the remark made in the documentation (under BadPrecondition : https://github.com/LeventErkok/sbv/blob/master/Data/SBV/Tools/WeakestPreconditions.hs#L135), since within wpProveWith we clearly have a precondition check ( https://github.com/LeventErkok/sbv/blob/master/Data/SBV/Tools/WeakestPreconditions.hs#L221) .

Is there a way to emit a BadPrecondition instead?

LeventErkok commented 2 months ago

Note the line:

               constrain $ sNot $ precondition start .=> sAnd (map fst vcs)

simply constrains the proof to all starting states that satisfy the precondition. If your precondition is badly formulated (for instance, if it is const sFalse), then it'll be the same as constrain sFalse; i.e., all proofs will trivially pass. (It's equivalent to proving sFalse .=> anything. (In other words, the state space is empty.)

When you do a traceExecution we'll explicitly check that the concrete state you provide satisfies the precondition, and then we can warn the user if that's not the case. (In other words, you've given a starting state that's not valid.)

ocramz commented 2 months ago

Thank you! Now it makes a lot of sense. I hadn't investigated the mechanics of the Query monad.

LeventErkok commented 2 months ago

This has nothing to do with queries. I’m not sure if I understand your comment.

ocramz commented 2 months ago

apologies, I meant SymbolicT . Mixed up