From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: border1.nntp.ams.giganews.com!nntp.giganews.com!news.mixmin.net!newsfeed.fsmpi.rwth-aachen.de!news-1.dfn.de!news.dfn.de!news.uni-weimar.de!medsec1.medien.uni-weimar.de!lucks From: Stefan.Lucks@uni-weimar.de Newsgroups: comp.lang.ada Subject: Re: The future of Spark . Spark 2014 : a wreckage Date: Thu, 11 Jul 2013 21:23:29 +0200 Organization: Bauhaus-Universitaet Weimar Message-ID: References: NNTP-Posting-Host: medsec1.medien.uni-weimar.de Mime-Version: 1.0 Content-Type: MULTIPART/MIXED; BOUNDARY="8323329-1242834904-1373570610=:8707" X-Trace: tigger.scc.uni-weimar.de 1373570526 15294 141.54.178.228 (11 Jul 2013 19:22:06 GMT) X-Complaints-To: news@tigger.scc.uni-weimar.de NNTP-Posting-Date: Thu, 11 Jul 2013 19:22:06 +0000 (UTC) X-X-Sender: lucks@debian In-Reply-To: User-Agent: Alpine 2.10 (DEB 1266 2009-07-14) Xref: number.nntp.dca.giganews.com comp.lang.ada:182467 Date: 2013-07-11T21:23:29+02:00 List-Id: This message is in MIME format. The first part should be readable text, while the remaining parts are likely unreadable without MIME-aware tools. --8323329-1242834904-1373570610=:8707 Content-Type: TEXT/PLAIN; charset=ISO-8859-15; format=flowed Content-Transfer-Encoding: QUOTED-PRINTABLE On Wed, 10 Jul 2013, Randy Brukardt wrote: >> Secondly, Ada's "in", "out", and "in out" information give only a cursor= y >> view of what is going on. > > Of course. But that and the postcondition is all you ought to be dependin= g > 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=20 proven) in the specification. Which is one reason why "Depends" is=20 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 eve= n 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=20 flow analysis actually catches a lot of errors -- even without having=20 specified any pre- or postconditions. In other words, SPARK's information= =20 flow analysis actually gives you the low-hanging fruits you mention. The fruits (well, bugs) you catch by employing pre- and postconditions are= =20 a bit higher, actually. At least, that is what I gather from my own=20 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=E4t Weimar, Germany-- --8323329-1242834904-1373570610=:8707--