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: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!gandalf.srv.welterde.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED.rrsoftware.com!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: Tests in a software release
Date: Tue, 14 Nov 2017 18:01:28 -0600
Organization: JSA Research & Innovation
Message-ID: <oug04o$h02$1@franka.jacob-sparre.dk>
References: <osqoph$1ves$1@gioia.aioe.org> <oss2c3$1p2m$1@gioia.aioe.org>
 <osvsjs$t4b$1@dont-email.me> <osvvds$s97$1@gioia.aioe.org>
 <ot19fo$7mi$2@dont-email.me> <ot1bvm$ub7$1@gioia.aioe.org>
 <ot82v3$h2c$1@dont-email.me> <ot83l0$1rb1$1@gioia.aioe.org>
 <ot981s$7m5$1@dont-email.me>
Injection-Date: Wed, 15 Nov 2017 00:01:29 -0000 (UTC)
Injection-Info: franka.jacob-sparre.dk;
 posting-host="rrsoftware.com:24.196.82.226";
	logging-data="17410"; mail-complaints-to="news@jacob-sparre.dk"
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.7246
Xref: feeder.eternal-september.org comp.lang.ada:48897
Date: 2017-11-14T18:01:28-06:00
List-Id: <comp.lang.ada>

"G.B." <bauhaus@notmyhomepage.invalid> wrote in message 
news:ot981s$7m5$1@dont-email.me...
...
> Checking is behavior. However, let SPARK check conditions
> of a contract, and let the result be Truth. Then they
> have been checked before the program even runs, and
> turning *off* Ada checks is, therefore, justified.

Yes, but a compiler can do this better, since it knows the actual 
representations chosen (which might ensure that a check cannot fail where 
SPARK may not be able to prove this, at least not without lots of additional 
information). Moreover, a compiler surely knows if it generated code to 
raise Constraint_Error.

Ergo, I would much prefer to trust the compiler (and if you can't trust your 
compiler, you have a serious problem that no other tool is going to be able 
to help with) rather than having to trust an entire chain of tools that 
necessarily has to include the compiler.

There are lots of things that SPARK can prove that a compiler can't, but 
there aren't many (if any) check eliminations that require the power of 
SPARK (and I believe that the vast majority of those can be fixed with the 
addition of additional tests or subtypes).

                                  Randy.