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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no 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: "G.B." <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: {Pre,Post}conditions and side effects
Date: Fri, 24 Apr 2015 18:29:51 +0200
Organization: A noiseless patient Spider
Message-ID: <mhdr01$lrf$1@dont-email.me>
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>	<mhdbpc$pl6$1@dont-email.me>
 <87oamdlhd3.fsf@adaheads.sparre-andersen.dk>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Fri, 24 Apr 2015 16:28:49 +0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="b96887e80893c84a90c3007226ca0d1c";
	logging-data="22383"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19ot3tk7nQOQ2dT9T023477hgGpdfu6VdA="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9;
 rv:31.0) Gecko/20100101 Thunderbird/31.6.0
In-Reply-To: <87oamdlhd3.fsf@adaheads.sparre-andersen.dk>
Cancel-Lock: sha1:CioHJMeSJgvYu/IeSF1QD10ArqU=
Xref: news.eternal-september.org comp.lang.ada:25599
Date: 2015-04-24T18:29:51+02:00
List-Id: <comp.lang.ada>

On 24.04.15 16:40, Jacob Sparre Andersen wrote:
> "G.B." <bauhaus@futureapps.invalid> wrote:
>
> [...]
>
>> Last but not least, a precondition should never be anything but an
>> assumption. As not checking it at run-time is a valid way of handling
>> preconditions, the outcome of not tesing should still not create
>> havoc; so, the caller needs to make sure that assertion of the
>> contract is always true, and never depend on how it is tested, or on
>> that it is tested.
>
> Taking that view, there isn't any point combining the contract notation
> of Ada 2012 and SPARK 2014, as it would prevent you from writing a
> single source text which was valid for both languages.

That's hardly possible anyway, given the number of restrictions
that SPARK 2014 imposes, even when not taking assertions into account.
Is
   --# hide
all gone?

Also, why would there be a technical need to have a contract use
only Ada or SPARK 2014 as the single language? That's not done
in the LRM, which uses logic and mathematics; writing SPARK 2014,
non-SPARK compilers could simply omit analysis of the language used
in Pre => ... etc., presuming they can handle the syntax
(likely, I should think). And some things cannot reasonably be
stated formally anyway.  (I guess it becomes apparent that
maybe a combined language turns into a combined stricture! ;-)

The makers of, respectively, GNAT and SPARK have merged, that seems
like a start for better merging the languages; Tucker Taft,
now also at AdaCore, has alluded to excessive restrictions
in SPARK. The definitions of SPARK had added more of Ada over the
years already (tasks, tagged types, ...).

So, I guess, in the long run, there is no more risk of
Ada programs that suffer from conflicting language desires than
there is now when source texts show non-Ada 'Img and GNAT is
not your Ada compiler. ;-)