The loop invariants aren't part of the spec, they're part of the proof, and the computer's job is to automate as much of the proof as it can. That being said, automatically finding loop invariants is a hard and messy problem, so I can't really blame the Frama-C authors.

The loop invariants that you can detect may not be the loop invariants that they want. Consider:

  for(int i = 0; i < n; i++) {..}

It looks like the invariant should be:

  0 <= i < n

But if they mistyped the loop that would be wrong. You have to explicitly state your invariants. At best, you could detect them and ask for confirmation. And that's for an easy to detect case.

This sounds like an invariant even an optimizing compiler could find, because it's such a common construct. Well... I guess they have an easier job because they can "assume away" signed overflow.

My point was that that may not be the actual invariant. By making your invariants explicit these tools have a better chance of finding real errors since you compare the code against a specification. Deriving a specification just means your code works according to itself.

Presumably, you are doing something other than just incrementing i in the loop, though.

Most of the time with Frama-C, all you have to provide is function pre- and post-conditions and loop invariants.

What programs can do is "loop invariant synthesis" (for people that want to google it), this is still quite tricky to do. There's a reason that humans also find loop invariants tricky.

In fact that would be

``` 0 <= i <= n ```

As the loop reaches this value to terminate. Else, we could not deduce for example that `i = n` at the end of the loop (`0 <= i <= n && !(i < n)`).

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.

What? 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?