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!feeder.eternal-september.org!gandalf.srv.welterde.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: {Pre,Post}conditions and side effects
Date: Mon, 11 May 2015 19:30:45 -0500
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <mirhjl$kvm$1@loke.gir.dk>
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>
NNTP-Posting-Host: rrsoftware.com
X-Trace: loke.gir.dk 1431390646 21494 24.196.82.226 (12 May 2015 00:30:46 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Tue, 12 May 2015 00:30:46 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-RFC2646: Format=Flowed; Original
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157
Xref: news.eternal-september.org comp.lang.ada:25822
Date: 2015-05-11T19:30:45-05:00
List-Id: <comp.lang.ada>

"Paul Rubin" <no.email@nospam.invalid> wrote in message 
news:87pp6a1u9w.fsf@jester.gateway.sonic.net...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
>> For example, in this "Is_Sorted" example, if you are assuming that some
>> object is sorted, then it should have a predicate to that effect.
>
> Randy, is that a real possibility with SPARK--to have a predicate that
> says that an array is sorted and have it verified at compile time by the
> compiler?  I thought SPARK mostly was for proving rather simpler
> conditions.

I have no idea, SPARK is not at all my idea of how Ada should work.

Ada 2012 surely does have predicates, and one hopes that Ada 202x has 
exception contracts, blocking contracts, global data contracts, and anything 
else needed to do useful data flow proving. (Most of that is already 
started, but who knows if any of it will get finished?)

                                      Randy.