Allow better insight into where a proof failed

team-worthwhile / worthwhile

PSE am KIT 2011/12: Programmverifikation (Team 2)

BSD 3-Clause "New" or "Revised" License

5 stars 3 forks source link

Allow better insight into where a proof failed #15

Closed bafain closed 12 years ago

bafain commented 12 years ago

When calculating the weakest precondition in WPStrategy, beginning with the last program statement, push a new weakest precondition on a stack (which has to be added to all others currently on the stack, too) whenever an assertion is visited. Afterwards pop the stack in SpecificationChecker, check the validity with a prover, notify your observers about the result (see the already added AbstractProverEventListener) and go on with the next stack item.

leonhandreke commented 12 years ago

See 672a5bb8672fdb22255a0cf776c36fa651b87a58 for an initial attempt to implement this feature.

leonhandreke commented 12 years ago

The branch feature/partial-proofs contains several commits working towards the goal described above. 2788415bcb2a271e6a5c4ef46fe82a0997e809d7 already works pretty well.

Remaining tasks that I can think of from the top of my head:

Add proof tasks to prove a whole Conditional, Loop or FunctionDeclaration. Likely a conjunction of all the individual proofs.
Better deal with division by zero by marking the problematic expression.

leonhandreke commented 12 years ago

Bugs have been opened for the remaining issues. Closing.