4 ms·

>I had to provide my own loop invariants, which is also a pain You either make your spec up as you go along and don't check it as its hidden in the code, or pr

>I had to provide my own loop invariants, which is also a pain You either make your spec up as you go along and don't check it as its hidden in the code, or provide it so that static analysis tools and/or things like tla+ can help confirm. There never was any getting around that regardless of language. The code follows from spec which both follow from requirements

creata 6y ago
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.
- 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 ago
    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?
- Jtsummers 6y ago
  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.
  - the-smug-one 6y ago
    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.
  - im3w1l 6y ago
    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.
    - Jtsummers 6y ago
      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.
    - mcguire 6y ago
      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.
  - KsassPeuk 6y ago
    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)`).

creata 6y ago

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.

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 ago
  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?
Jtsummers 6y ago
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.
- the-smug-one 6y ago
  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.
- im3w1l 6y ago
  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.
  - Jtsummers 6y ago
    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.
  - mcguire 6y ago
    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.
- KsassPeuk 6y ago
  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)`).