SPARK - refactoring and refinement of own state

SPARK - refactoring and refinement of own state

[Maciej Sobczak]

I have a problem that can be reduced to a simple hello world program
in SPARK.
Consider the following:

with Spark_IO;
--# inherit Spark_IO;

--# main_program;
procedure Hello
  --# global in out Spark_IO.Outputs;
  --# derives Spark_IO.Outputs from *;
is
begin
   Spark_IO.Put_String (File => Spark_IO.Standard_Output,
                        Item => "Hello ",
                        Stop => 0);
end Hello;

Let's suppose that I want to refactor it a bit and move the details of
printing to some other package and use that other package from the
main program. In other words, I want to isolate the main program from
Spark_IO.
Consider this package spec:

package Greetings
  --# own State;
  --# initializes State;
is

   procedure Say_Hello;
   --# global in out State;
   --# derives State from *;

end Greetings;

The main program then becomes:

with Greetings;
--# inherit Greetings;

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

The SPARK Examiner is happy with both the main program and the spec
for the Greetings package.

The problem is with the package body.
This is what I believe should work:

with Spark_IO;
--# inherit Spark_IO;

package body Greetings
  --# own State is Spark_IO.Outputs;
is

   procedure Say_Hello
     --# global in out Spark_IO.Outputs;
     --# derives Spark_IO.Outputs from *;
   is
   begin
      Spark_IO.Put_String (File => Spark_IO.Standard_Output,
                           Item => "Hello ",
                           Stop => 0);
   end Say_Hello;

end Greetings;

However, the examiner says:

   4  package body Greetings
              ^
***        Syntax Error      : No DOTTED_SIMPLE_NAME can start with
reserved
           word "BODY".

What is most interesting is that after removing the inherit clause
from the package body the examiner no longer complains about the
"body" keyword, but of course fails later on with the "Spark_IO"
procedure prefix, which is reported as undeclared or not visible
(semantic error 142).

The whole problem is really about refining the own state of some
package in terms of the abstract own state of some other package. I
have not found anything about this in the SPARK documentation and the
error message about the "body" keyword is confusing.

Am I going in the right direction anyway? Is this kind of refactoring
and refinement possible?

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

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

Re: SPARK - refactoring and refinement of own state

[Georg Bauhaus]

Maciej Sobczak wrote:

> However, the examiner says:
> 
>    4  package body Greetings
>               ^
> ***        Syntax Error      : No DOTTED_SIMPLE_NAME can start with
> reserved
>            word "BODY".

FWIW, there is a rule about Ada with-ing versus SPARK with-ing
that explains, IIRC, that the #clauses must go before
the package spec, in SPARK, not just the body. It's in the
SPARK book somewhere.

Re: SPARK - refactoring and refinement of own state

[Rod Chapman]

On Aug 20, 8:37 am, Georg Bauhaus <rm.tsoh.plus-
bug.bauh...@maps.futureapps.de> wrote:
> Maciej Sobczak wrote:
> > However, the examiner says:
>
> >    4  package body Greetings
> >               ^
> > ***        Syntax Error      : No DOTTED_SIMPLE_NAME can start with
> > reserved
> >            word "BODY".
>
> FWIW, there is a rule about Ada with-ing versus SPARK with-ing
> that explains, IIRC, that the #clauses must go before
> the package spec, in SPARK, not just the body. It's in the
> SPARK book somewhere.

Yeah - the "inherit" anno always goes on the spec.  In this
case the Examiner see the "inherit" and then expects to see
a package spec, so then objects when the word "body" appears.

We'll see if we can generate a better error message for this case.
 - Rod, SPARK Team

Re: SPARK - refactoring and refinement of own state

[Rod Chapman]

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

Re: SPARK - refactoring and refinement of own state

[Maciej Sobczak]

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