On 6/26/14, 4:16 PM, Timon Gehr wrote:
- Annotations can include a formal proof.
If a function can be annotated with what other functions it calls (non-transitively), I agree that it can be guaranteed with local semantic checking that a program won't overflow. However requiring such annotations would be onerous, and deducing them would require whole program analysis.
We've had similar discussions before. Why do we _still_ have to argue about the _possibility_ of having a system that is helpful for proving stack overflows (or other bad behaviours) absent? You can say "out of scope" or "not a priority" or "this should be realized in third-party tool support" but not "it is impossible".
I also seem to reckon Walter is in the other extreme (he asserts it can't be done at all, period). My understanding is that it can be done but only with annotations or whole program analysis.
Andrei
