On Wed, 10 Jul 2013, Randy Brukardt wrote: >> Secondly, Ada's "in", "out", and "in out" information give only a cursory >> view of what is going on. > > Of course. But that and the postcondition is all you ought to be depending > upon. If you're depending on more, your program is more fragile than it > ought to be. Your program can depend on whatever has been specified (and hopefully proven) in the specification. Which is one reason why "Depends" is actually useful -- you are allowed to make more specific contracts. > ... (detailed and possibly interesting examples of Depends removed) > > ... >> Without "Depends", your cool analysis tool verifying all pre- and >> postconditions will not catch this bug. > > Sure, but so what? It's a fools game to try to catch all bugs, it not even a > worthwhile goal. (That's essentially where Spark goes wrong, in my view.) Who said, catch all bugs? I didn't. > What I care about is extending what Ada already does well: catch the > low-hanging fruit of bugs. By my own experience, having worked occasionally with SPARK, information flow analysis actually catches a lot of errors -- even without having specified any pre- or postconditions. In other words, SPARK's information flow analysis actually gives you the low-hanging fruits you mention. The fruits (well, bugs) you catch by employing pre- and postconditions are a bit higher, actually. At least, that is what I gather from my own experience YMMV. Did you ever actually work with SPARK? So long Stefan ------ I love the taste of Cryptanalysis in the morning! ------ --Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany--