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
238 stars 33 forks source link

Q: Results of 'wpProveWith' #697

Closed ocramz closed 2 months ago

ocramz commented 2 months ago

Hi, I am playing with the WeakestPreconditions module and realized I don't fully understand what does wpProveWith do, namely what does it exactly prove when it emits "QED".

Since we specify a global pre- and post-condition P and Q as part of the program S, is total correctness established when the computed WP is equivalent (in some sense) to P ?

LeventErkok commented 2 months ago

The semantics is that of Hoare logic: https://en.wikipedia.org/wiki/Hoare_logic

If you see QED, that'd mean your algorithm would always terminate and when it does, it will always guarantee the post-condition Q when it does; assuming P holds before the program starts execution.

The way the algorithm works is by computing a weakest-precondition that is required to establish the post-condition; and showing that your initial pre-condition implies this weakest-precondition. But there's nothing SBV specific here; this is standard Hoare logic and the weakest precondition calculus; as established by Dijkstra in his predicate transformers work. See: https://en.wikipedia.org/wiki/Predicate_transformer_semantics

(Of course all of this is modulo any bugs SBV might have: The weakest-precondition code hasn't been all that well tested; if you find any issues please file them and PR's fixing them are also appreciated.) There're a bunch of examples here: https://github.com/LeventErkok/sbv/tree/master/Documentation/SBV/Examples/WeakestPreconditions

ocramz commented 2 months ago

Thank you,

showing that your initial pre-condition implies this weakest-precondition

This is the answer to my question.