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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no 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!o35g2000vbi.googlegroups.com!not-for-mail
From: Maciej Sobczak <see.my.homepage@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK - refactoring and refinement of own state
Date: Thu, 20 Aug 2009 01:44:54 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <fde732b8-4926-4c8d-b797-60cfda085296@o35g2000vbi.googlegroups.com>
References: 
 <4cc6e9da-9a4a-4a9a-8748-4c5c4a3e9362@z28g2000vbl.googlegroups.com>
	<88ecb7be-ade2-4d0b-8063-fa06d53be1e8@e34g2000vbm.googlegroups.com>
NNTP-Posting-Host: 137.138.182.236
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
X-Trace: posting.google.com 1250757894 17656 127.0.0.1 (20 Aug 2009 08:44:54
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Thu, 20 Aug 2009 08:44:54 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: o35g2000vbi.googlegroups.com; posting-host=137.138.182.236;
	posting-account=bMuEOQoAAACUUr_ghL3RBIi5neBZ5w_S
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.5; en-US;
	rv:1.9.1.2) Gecko/20090729 Firefox/3.5.2,gzip(gfe),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:7905
Date: 2009-08-20T01:44:54-07:00
List-Id: <comp.lang.ada>

On 20 Sie, 10:11, Rod Chapman <roderick.chap...@googlemail.com> wrote:

> 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.

Or rather it doesn't preserve the information about state coupling.

Indeed, the grammar allows the inherit clause only in the package spec
(I was confused about that as well).

Just for completeness, the program after "refactoring" is:

-- greetings.ads:
with Spark_IO;
--# inherit Spark_IO;

package Greetings
is

   procedure Say_Hello;
   --# global in out Spark_IO.Outputs;
   --# derives Spark_IO.Outputs from *;

end Greetings;

-- greetings.adb:
package body Greetings
is

   procedure Say_Hello
   is
   begin
      Spark_IO.Put_String (File => Spark_IO.Standard_Output,
                           Item => "Hello ",
                           Stop => 0);
   end Say_Hello;

end Greetings;

-- hello.adb:
with Greetings;
--# inherit Greetings, Spark_IO;

--# main_program;
procedure Hello
  --# global in out Spark_IO.Outputs;
  --# derives Spark_IO.Outputs from *;
is
begin
   Greetings.Say_Hello;
end Hello;

This shows that state coupling cannot be hidden (unless it is
hidden :-) ).

Thank you for explanations.

--
Maciej Sobczak * www.msobczak.com * www.inspirel.com

Database Access Library for Ada: www.inspirel.com/soci-ada