New answers tagged loop-invariants
3
Figure out what the value of y is, depending on x, a, and c. Prove that your formula is correct before the first iteration, and prove that if it is true before an iteration then it is also true after the iteration.
3
By a happy coincidence, people (Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz and Laurent Thery) have completed formally verified implementations of Tarjan's algorithm in various formal systems!
The paper, titled "Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle", can be found, e.g. here.
One step of proving correctness in these ...
4
There will always be situations where we can see there is a complex invariant but the compiler cannot derive it. Type systems are sound but not complete: not all invariants can be expressed in the type system. So this isn't something specific to Tarjan's algorithm; it is a general fact of life when working in a type system -- sometimes the compiler will ...
Top 50 recent answers are included
