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
Path: 
 g2news1.google.com!news3.google.com!proxad.net!feeder1-2.proxad.net!news.in2p3.fr!in2p3.fr!kanaga.switch.ch!switch.ch!hefestos.uned.es!news.uv.es!not-for-mail
From: Manuel Collado <m.collado@domain.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Ada2012 Invariants and obaque types
Date: Tue, 21 Jun 2011 23:18:49 +0200
Organization: Universitat de Valencia
Message-ID: <itr255$3eq$1@peque.uv.es>
References: 
 <239a78ad-0937-4a7a-8163-231430fd5ffe@k27g2000yqn.googlegroups.com>
 <17t4afbmsrbm4.7llaajq91zz3.dlg@40tude.net> <op.vxfvc6uxule2fv@douda-yannick>
 <1rxmqjvvd0nk6.1pqiavml8xwzf.dlg@40tude.net>
NNTP-Posting-Host: 106.red-2-137-202.dynamicip.rima-tde.net
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 8bit
X-Trace: peque.uv.es 1308691429 3546 2.137.202.106 (21 Jun 2011 21:23:49 GMT)
X-Complaints-To: newsmanager@uv.es
NNTP-Posting-Date: Tue, 21 Jun 2011 21:23:49 +0000 (UTC)
User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; es-ES;
 rv:1.9.2.13) Gecko/20101207 Thunderbird/3.1.7
In-Reply-To: <1rxmqjvvd0nk6.1pqiavml8xwzf.dlg@40tude.net>
Xref: g2news1.google.com comp.lang.ada:19996
Date: 2011-06-21T23:18:49+02:00
List-Id: <comp.lang.ada>

El 21/06/2011 20:53, Dmitry A. Kazakov escribi�:
> On Tue, 21 Jun 2011 20:37:44 +0200, Yannick Duch�ne (Hibou57) wrote:
>
>> Le Tue, 21 Jun 2011 14:08:15 +0200, Dmitry A. Kazakov
>> <mailbox@dmitry-kazakov.de>  a �crit:
>>
>>> On Tue, 21 Jun 2011 01:53:31 -0700 (PDT), Martin wrote:
>>>
>>>> package P1 is
>>>>     type T1 is tagged private
>>>>        with Invariant =>  Is_Valid (T1);
>>>
>>> Unrelated to Ada, but in theory, an invariant is a private implementation
>>> dependent thing. An invariant is trivially true in all public views of
>>> the object,
>> I understand the point and had the same first feeling too.
>
> The first feeling is always the right one. (:-))
>
>> While that's OK
>> in theory, in practice the user may wish methods to check for validity
>> rules defined for a type.
>
> Validity is a misconception. In a properly typed language any value is
> valid, that is the property of being typed. A value is invalid when the
> type system was circumvented, which should never happen publicly.

Humm... What about an integral type whose set of valid values are the 
prime numbers (upto some representation limit)?

Common practice is to define such type as Integer, Natural or Positive, 
and write some validation function to check values at runtime.

Or do you mean that Ada is not a properly typed language?

-- 
Manuel Collado - http://lml.ls.fi.upm.es/~mcollado