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!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: {Pre,Post}conditions and side effects
Date: Tue, 12 May 2015 11:10:38 -0700
Organization: A noiseless patient Spider
Message-ID: <877fsd1xb5.fsf@jester.gateway.sonic.net>
References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com>
	<AnYlw.957256$Rp.242412@fx23.iad>
	<0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com>
	<wccoaqucn51.fsf@shell01.TheWorld.com>
	<9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com>
	<alpine.CYG.2.11.1412231747100.4196@WIL414CHAPIN.vtc.vsc.edu>
	<wccegrpq2om.fsf@shell01.TheWorld.com>
	<87tww5296f.fsf@adaheads.sparre-andersen.dk>
	<871tj9dp5b.fsf@theworld.com>
	<ce4af31e-d491-479f-a5b3-0b3eedea2a68@googlegroups.com>
	<midvq5$2u3$1@loke.gir.dk>
	<alpine.DEB.2.11.1505071103310.14859@debian>
	<migc9a$jp8$1@loke.gir.dk>
	<alpine.DEB.2.11.1505072052570.16448@debian>
	<mijen0$1hj$1@loke.gir.dk> <87pp6a1u9w.fsf@jester.gateway.sonic.net>
	<mirhjl$kvm$1@loke.gir.dk>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: mx02.eternal-september.org;
 posting-host="631d4aa67102f56712a7d69e4aea5bbf";
	logging-data="7170"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19TTS/WRg2xdHwbZpTPaLta"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux)
Cancel-Lock: sha1:L4vNL96swIoC9pxjPdDusLEzas0=
	sha1:YSxu6briKbQw4fGeNmbMZMsYchQ=
Xref: news.eternal-september.org comp.lang.ada:25844
Date: 2015-05-12T11:10:38-07:00
List-Id: <comp.lang.ada>

"Randy Brukardt" <randy@rrsoftware.com> writes:
>> Randy, is that a real possibility with SPARK--to have a predicate that
>> says that an array is sorted 
> I have no idea, SPARK is not at all my idea of how Ada should work.

Hmm, ok, I had been confused on that issue.  

So can you say what the predicate for a sorted array would look like in
Janus/ADA, and how the compiler would verify it?

Someone else mentioned that it can probably be done with Spark 2014
using so-called ghost functions, which is pretty cool, and I believe
surpasses the capabilities of Spark's earlier incarnations.