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.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,bd40601768eaf8fd
X-Google-Attributes: gid103376,public
From: "Matthew Heaney" <matthew_heaney@acm.org>
Subject: Re: 'constant functions' and access constant params (was Re: Array of
 Variant Records Question...)
Date: 1999/09/25
Message-ID: <37ec53ba@news1.prserv.net>#1/1
X-Deja-AN: 529311871
Content-transfer-encoding: 7bit
References: <7r5vh3$imu1@svlss.lmms.lmco.com> <37d6a45c@news1.prserv.net>
 <eExB3.6$ZR.1146@news.wenet.net> <37d6ccb6@news1.prserv.net>
 <7r77i8$i08$1@nnrp1.deja.com> <37d7c116@news1.prserv.net>
 <7r8t21$ov5$1@nnrp1.deja.com> <37d822a1@news1.prserv.net>
 <7reg02$t83@dfw-ixnews6.ix.netcom.com> <37DE8D09.C863CBC9@rational.com>
 <7roohh$s6r@dfw-ixnews7.ix.netcom.com> <37e01168@news1.prserv.net>
 <7rp86o$c6h@dfw-ixnews3.ix.netcom.com> <37E18CC6.C8D431B@rational.com>
 <7rs8bn$s6@dfw-ixnews4.ix.netcom.com> <37e2e58c@news1.prserv.net>
 <7s9nd0$cbe@dfw-ixnews17.ix.netcom.com> <37e8e067@news1.prserv.net>
 <7sas3p$bfa@dfw-ixnews3.ix.netcom.com> <37e994c0@news1.prserv.net>
 <wcchfkk2ocx.fsf@world.std.com>
Content-Type: text/plain; charset="US-ASCII"
X-Complaints-To: abuse@prserv.net
X-Trace: 25 Sep 1999 04:46:50 GMT, 129.37.213.219
Organization: Global Network Services - Remote Access Mail & News Services
Mime-version: 1.0
Newsgroups: comp.lang.ada
Date: 1999-09-25T00:00:00+00:00
List-Id: <comp.lang.ada>

In article <wcchfkk2ocx.fsf@world.std.com> , Robert A Duff 
<bobduff@world.std.com>  wrote:

> "Matthew Heaney" <matthew_heaney@acm.org> writes:
>
>> 2) For private types, I say the "stability of X" is a meaningless statement.
>> A supplier's only obligation is to satisfy the postcondition, which has
>> nothing to say about internal state changes.
>
> Please define exactly what you mean by "internal" state change.

External = public state  = partial view of type
Internal = private state = full view of type

For example, in Ada.Text_IO, the type is declared as

  type File_Type is limited private;

There is no external state.  The only thing I know (publicly) about File_Type
is what operations are available for it.

You could loosely refer to selector functions like Name or Is_Open as "external
state," but I'm not doing that here.  In a postcondition, I would state what
values those functions should return, but that's not quite what I mean by
external state (it's more like external "behavior").


> How can one tell the difference between internal and external
> state changes?

For a private type, there is no such thing as "external state," so this
question goes away.

Actually, that's a bit of a lie, since I could declare a tagged type this way:

  type T_Public is
    abstract tagged limited record
      I : Integer;
    end record;

  type T is
    new T_Public with private;

Here, objects of type T have some state that's external, namely component I.
But then it's easy to say what happens to the external state (I) in the
postcondition.


--
It is impossible to feel great confidence in a negative theory which has always
rested its main support on the weak points of its opponent.

Joseph Needham, "A Mechanistic Criticism of Vitalism"