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,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,48872198fdca5efd
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!postnews.google.com!e34g2000vbm.googlegroups.com!not-for-mail
From: Rod Chapman <roderick.chapman@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK - refactoring and refinement of own state
Date: Thu, 20 Aug 2009 01:11:12 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <88ecb7be-ade2-4d0b-8063-fa06d53be1e8@e34g2000vbm.googlegroups.com>
References: 
 <4cc6e9da-9a4a-4a9a-8748-4c5c4a3e9362@z28g2000vbl.googlegroups.com>
NNTP-Posting-Host: 217.205.167.137
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
X-Trace: posting.google.com 1250755872 11008 127.0.0.1 (20 Aug 2009 08:11:12
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Thu, 20 Aug 2009 08:11:12 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: e34g2000vbm.googlegroups.com; posting-host=217.205.167.137;
	posting-account=HCzrEgkAAABSfGsTnv-u5wET6EzuneVi
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-GB; rv:1.9.1.2)
	Gecko/20090729 Firefox/3.5.2 (.NET CLR 3.5.30729),gzip(gfe),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:7904
Date: 2009-08-20T01:11:12-07:00
List-Id: <comp.lang.ada>

As for refinement..

In short: refinement only makes sense _within_ a single
package, so you can only refine "onto" states which
are logically hidden inside the package body - so either library
level state in that package body, or states of private
child packages of that package.

So...no...you can't refine from one package body to the spec
of another package, since this doesn't preserve
the abstraction.
 - Rod