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!nntp-feed.chiark.greenend.org.uk!ewrotcd!newsfeed.xs3.de!io.xs3.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: Interesting article on ARG work
Date: Fri, 6 Apr 2018 21:01:47 -0500
Organization: JSA Research & Innovation
Message-ID: <pa98qb$ve2$1@franka.jacob-sparre.dk>
References: <p9s890$mmt$1@franka.jacob-sparre.dk>
 <1b44444f-c1b3-414e-84fb-8798961487c3@googlegroups.com>
 <62ee0aac-49da-4925-b9aa-a16695b3fc45@googlegroups.com>
 <pa0vga$rbe$1@franka.jacob-sparre.dk>
 <9879872e-c18a-4667-afe5-41ce0f54559f@googlegroups.com>
 <pa3jmj$9n3$1@franka.jacob-sparre.dk>
 <17b6d5b9-5909-4f0c-ab25-9b3cf4fd0450@googlegroups.com>
 <pa66vj$20n$1@franka.jacob-sparre.dk>
 <2be6c759-1a2f-48fc-81b1-ffab1d1c957d@googlegroups.com>
Injection-Date: Sat, 7 Apr 2018 02:01:48 -0000 (UTC)
Injection-Info: franka.jacob-sparre.dk;
 posting-host="rrsoftware.com:24.196.82.226";
	logging-data="32194"; 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; Original
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.7246
Xref: reader02.eternal-september.org comp.lang.ada:51368
Date: 2018-04-06T21:01:47-05:00
List-Id: <comp.lang.ada>


"Bojan Bozovic" <bozovic.bojan@gmail.com> wrote in message 
news:2be6c759-1a2f-48fc-81b1-ffab1d1c957d@googlegroups.com...
...
>If assertions/invariants encompassed type invariants and were used
>in loops as well, like in Eiffel, readability would be better in my
>humble opinion, while Ada have pragma assert that can be used in
>loops, and static_predicate and dynamic_predicate on types.
>
>Maybe assertion blocks would work better as in Eiffel for loops?
>Like exception block in Ada?

No idea. There are definitely other kinds of contracts not currently defined 
in Ada -- loop invariants certainly are one of those. Ada 2020 adds 
Default_Initial_Condition as a contract, and Stable_Properties as a 
technique for managing contracts (postconditions). We haven't talked much 
about other contracts, but certainly we'll do so in the future.

Such contracts would certainly in addition to pragma Assert (which is 
general, but completely manual). And of course the form hasn't been decided.

Giving a different form to existing contracts isn't likely to get much 
interest. Additional contracts might (or might) be different.

                          Randy.