Re: SPARK - refactoring and refinement of own state

[Maciej Sobczak <see.my.homepage@gmail.com>]

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