From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on
	ip-172-31-74-118.ec2.internal
X-Spam-Level: 
X-Spam-Status: No, score=-0.5 required=3.0 tests=BAYES_05 autolearn=ham
	autolearn_force=no version=3.4.4
Path: eternal-september.org!reader01.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: My new post on dev.to about SPARK
Date: Thu, 09 Jul 2020 23:04:03 -0700
Organization: A noiseless patient Spider
Message-ID: <875zav52jw.fsf@nightsong.com>
References: <8e5d14a5-0311-4005-9655-951e8a274929o@googlegroups.com>
	<lyh7ugcvcd.fsf@pushface.org> <re8q4i$rk3$1@dont-email.me>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org; posting-host="2142c6408383bca8a8acc95edb5b7597";
	logging-data="13524"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+0eMyMJEM+HEVo+kdbQJWi"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (gnu/linux)
Cancel-Lock: sha1:y2l8Tg2kowwKdC1SDx9R3AkwJhk=
	sha1:RYZRtih+E/nWg/uHEii6ryMkV2Q=
Xref: reader01.eternal-september.org comp.lang.ada:59421
List-Id: <comp.lang.ada>

"J-P. Rosen" <rosen@adalog.fr> writes:
> Hmmm.. The following O(N**2) function: ...
> can be changed to a O(N) function:
> function Is_Sorted (Table : Array_Type) return Boolean
>    is (for all L in Table'First .. Table'Last -1 =>
>             Table (L) < Table (L+1))
>    with Ghost;

Should it matter?  The code is never executed.  It's only used as a
specification for the theorem prover.

By the way, Riccardo, thanks for posting that.  It was impressive to see
that an executable-looking spec like that could be proved automatically
with the help of just a few pragmas.  I hadn't posted yet because I
haven't yet had a chance to try building and playing with the program.