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=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,ad06d2d7cb045687
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.135.231 with SMTP id pv7mr229857pbb.8.1328757063515;
        Wed, 08 Feb 2012 19:11:03 -0800 (PST)
MIME-Version: 1.0
Path: 
 wr5ni3418pbc.0!nntp.google.com!news2.google.com!goblin2!goblin.stu.neva.ru!newsfeed.x-privat.org!news.jacob-sparre.dk!pnx.dk!jacob-sparre.dk!ada-dk.org!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: Silly and stupid post-condition or not ?
Date: Wed, 8 Feb 2012 21:10:59 -0600
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <jgvdg5$2cm$1@munin.nbi.dk>
References: <op.v8w6ptk5ule2fv@douda-yannick>
 <82wr86fzos.fsf@stephe-leake.org>
 <5af407fc-2868-44ca-84d2-c51a2a64104d@o4g2000pbc.googlegroups.com>
 <82k445fu9n.fsf@stephe-leake.org> <jgfjc4$u4b$1@munin.nbi.dk>
 <MPG.29972ec7befb6ae9989682@news.zen.co.uk> <jgl70g$l9i$1@munin.nbi.dk>
 <jgq2j2$g67$1@dont-email.me>
NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net
X-Trace: munin.nbi.dk 1328757061 2454 69.95.181.76 (9 Feb 2012 03:11:01 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Thu, 9 Feb 2012 03:11:01 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-RFC2646: Format=Flowed; Response
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157
Date: 2012-02-08T21:10:59-06:00
List-Id: <comp.lang.ada>

"BrianG" <me@null.email> wrote in message news:jgq2j2$g67$1@dont-email.me...
...
> It sounds like you don't want SPARK (as it is now, at least), but 
> something like an Ada equivalent to LINT.  (Not an Ada version of lint, 
> but something that does for Ada what lint does for C - covers Ada's needs, 
> rather than C's.)

It's not "Lint" really, it's really something to find errors of omission. 
(Errors of commission are many times easier to find and fix, like using the 
wrong algorithm or subtracting rather than adding.)

And usually this boils down to proving the absence of and/or proper handling 
of exceptions. 90% of the interesting cases have something to do with 
exceptions: either exceptions that are raised when they're not expected or 
not handled when they are expected.

I also want to do this in the context of normal compilation, so that (a) 
there is immediate feedback about problems and (b) there is no temptation to 
skip the step and (c) because I'm not in a position to build another large 
tool. ;-)

OK, the last probably isn't that important, but finding out about the 
problems as early as possible is important.

                                            Randy.