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,146d9a693430fff2
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!news1.google.com!news.glorb.com!feeder.erje.net!newsreader5.netcologne.de!news.netcologne.de!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Tue, 21 Jun 2011 15:29:22 +0200
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.6; en-US;
 rv:1.9.2.17) Gecko/20110414 Thunderbird/3.1.10
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: Ada2012 Invariants and obaque types
References: 
 <239a78ad-0937-4a7a-8163-231430fd5ffe@k27g2000yqn.googlegroups.com>
 <17t4afbmsrbm4.7llaajq91zz3.dlg@40tude.net>
 <4e008bc8$0$6568$9b4e6d93@newsspool3.arcor-online.net>
 <12jyfk40laprz.1mxczd0ze0dr7.dlg@40tude.net>
In-Reply-To: <12jyfk40laprz.1mxczd0ze0dr7.dlg@40tude.net>
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Message-ID: <4e009cb2$0$6582$9b4e6d93@newsspool3.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 21 Jun 2011 15:29:22 CEST
NNTP-Posting-Host: 1e756d99.newsspool3.arcor-online.net
X-Trace: 
 DXC=47ll]7]<45WE47KDAk81NWMcF=Q^Z^V3X4Fo<]lROoRQ8kF<OcfhCO[D3VD?Y_Xj[Ync\616M64>ZLh>_cHTX3j]ll[b\`<ilf_
X-Complaints-To: usenet-abuse@arcor.de
Xref: g2news1.google.com comp.lang.ada:19988
Date: 2011-06-21T15:29:22+02:00
List-Id: <comp.lang.ada>

On 21.06.11 14:31, Dmitry A. Kazakov wrote:

>> In another theory, the invariant may express things
>> such as
>>  Num_Green_Lights (T1) >= 3;
>> or
>> 'Length < State_of_Things (T1) * 2;
>> where Num_Green_Lights is a publicly visible function whose
>> result is somehow computed.  These predicates would be informative,
>> and formal.
> 
> That is not an invariant, but a constraint.

I don't see bounds in the above.

I can state, though, that there will be---invariably---at least
three green lights because that is a property of how each
implementation of the type will be constructed.  How is that
variant?  That is, if the (theoretical) assertion is "at least,
no matter what, under all circumstances, in each implementation",
isn't this an invariant?