4 ms·
Wait - what are you arguing? That Frama or some other code can come up with loop invariants by itself from the code? Even if this is true and doable, it's bad.
by doonesbury 6y ago
Wait - what are you arguing? That Frama or some other code can come up with loop invariants by itself from the code? Even if this is true and doable, it's bad. The question always was: does the code satisfy the spec, not whether we can derive a spec from the code and prove the spec is valid. In the other case - no - it's just what I wrote above.
- creata 6y agoWhat? The loop invariants aren't part of the spec! The loop invariants are just an intermediate step in your proof that the preconditions are enough to guarantee that the postconditions will hold. If I was proving that 0 + 1 + .. n = n(n+1)/2, I wouldn't say that whatever induction step I chose to use was "part of the theorem", would I?