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=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,23c0de5a42cf667e
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!news2.google.com!npeer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!nntp.club.cc.cmu.edu!micro-heart-of-gold.mit.edu!newsswitch.lcs.mit.edu!nntp.TheWorld.com!not-for-mail
From: Robert A Duff <bobduff@shell01.TheWorld.com>
Newsgroups: comp.lang.ada
Subject: Re: GNAT packages in Linux distributions
Date: Fri, 14 May 2010 20:17:30 -0400
Organization: The World Public Access UNIX, Brookline, MA
Message-ID: <wccocgij9wl.fsf@shell01.TheWorld.com>
References: <j5e1x31qvn1b$.11ywrjmshtauz$.dlg@40tude.net>
 <87mxw9x7no.fsf@ludovic-brenta.org>
 <t8liq7w6ffnm$.19yq5hkq6tdto$.dlg@40tude.net> <op.vcgi9oqzule2fv@garhos>
 <w1q9e75h9kzi.4p81vh3kannn$.dlg@40tude.net> <op.vch6dsqmxmjfy8@garhos>
 <16bz9kvbqa8y9$.155ntpwpwl29d.dlg@40tude.net>
 <4be97bea$0$2966$ba4acef3@reader.news.orange.fr> <op.vcjtnsp5xmjfy8@garhos>
 <quqkqeas8pu2$.1w5pelct29juv.dlg@40tude.net>
 <Pine.LNX.4.64.1005121017020.21749@medsec1.medien.uni-weimar.de>
 <1p87qdlnjbufg.127laayhrw9x3$.dlg@40tude.net> <op.vclocqp9ule2fv@garhos>
 <4j73xhgimt6r$.pu55kne2p2w5$.dlg@40tude.net>
 <4beaeeed$0$6888$9b4e6d93@newsspool2.arcor-online.net>
NNTP-Posting-Host: shell01.theworld.com
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Trace: pcls4.std.com 1273882638 26135 192.74.137.71 (15 May 2010 00:17:18
 GMT)
X-Complaints-To: abuse@TheWorld.com
NNTP-Posting-Date: Sat, 15 May 2010 00:17:18 +0000 (UTC)
User-Agent: Gnus/5.1008 (Gnus v5.10.8) Emacs/21.3 (irix)
Cancel-Lock: sha1:MBgaiXTj9j33AffVOcFl34zAWyY=
Xref: g2news2.google.com comp.lang.ada:11625
Date: 2010-05-14T20:17:30-04:00
List-Id: <comp.lang.ada>

Georg Bauhaus <rm.dash-bauhaus@futureapps.de> writes:

> How would you specify
>
>    subtype Even is ...; ?

In Ada 2012, if AI-153 gets approved, you will be able to say:

    subtype Even is Integer
        with Predicate => (Even mod 2) = 0;
                           ^^^^ refers to the "current instance"
                                of the subtype

That particular example isn't very useful, but this kind of
thing is:

    type Color is (Red, Orange, Yellow, Green, Blue);
    subtype Primary_Color is Color
        with Predicate => Primary_Color in (Red, Green, Blue);

By the way, I don't think "static" is a property of assertions.
It's a property of how they're checked.  If we have
a precondition that "X > Y" (where X and Y are formal parameters),
that's neither "static" nor "dynamic" in and of itself.
One tool (e.g. an Ada compiler) might check it dynamically.
A smarter tool (a proof checker, or a smarter compiler,
or even a human being) might check it statically.
It might even be checked statically at some call sites,
but not others.

- Bob