On Thursday, 7 August 2014 at 08:52:43 UTC, Matthias Bentrup
wrote:
So reachability has an influence, but control flow hasn't ?
You have to define what you want to prove.
1. The post condition to hold?
2. A sound specification to be fully implemented?
3. That executed code is tested when it executes, but ignore that
important code should have been executed instead.
(1) and (2) is what program verification and aims for.
(1) is what design by contract tries to establish.
(3) is weak and what c-asserts do.
