How to put main procedure in SPARK_Mode?

How to put main procedure in SPARK_Mode?

[mockturtle]

Dear.all,
this is really a silly questions, but I am stumped...

I am fooling around with SPARK (I always wanted to learn to use it) and I want to put the "main" procedure (that is in a body file of its own) in SPARK_Mode, but with no success so far.  

I tried many things including (but not limited to :-))
 
* Using Pragma SPARK_Mode (with and without "On") at the beginning of the file

* Using Pragma SPARK_MODE after the "is" 

* Using 
  procedure Main with SPARK_Mode => is ....

and other variations that I do not remember.

The only way I was able to put the procedure in SPARK mode is by putting it into a package, but in this way it cannot be the "main" (right?).  I solved the problem by having a microscopic main procedure whose only action is to call the true main in the package, but it seems to me less than ideal... 

Any suggestions?

Thank you in advance

Riccardo

Re: How to put main procedure in SPARK_Mode?

[Simon Wright]

mockturtle <framefritti@gmail.com> writes:

> I am fooling around with SPARK (I always wanted to learn to use it)
> and I want to put the "main" procedure (that is in a body file of its
> own) in SPARK_Mode, but with no success so far.
>
> I tried many things including (but not limited to :-))
>  
> * Using Pragma SPARK_Mode (with and without "On") at the beginning of
>   the file
>
> * Using Pragma SPARK_MODE after the "is" 
>
> * Using 
>   procedure Main with SPARK_Mode => is ....
>
> and other variations that I do not remember.
>
> The only way I was able to put the procedure in SPARK mode is by
> putting it into a package, but in this way it cannot be the "main"
> (right?).  I solved the problem by having a microscopic main procedure
> whose only action is to call the true main in the package, but it
> seems to me less than ideal...
>
> Any suggestions?

I just tried

   project Spark_Main is
      for Source_Files use ("spark_main.adb");
   end Spark_Main;

and

   procedure Spark_Main with SPARK_Mode is
   begin
      null;
   end Spark_Main;

and it worked OK.

Re: How to put main procedure in SPARK_Mode?

[mockturtle]

On Tuesday, May 21, 2019 at 4:14:44 PM UTC+2, Simon Wright wrote:
> mockturtle <framefritti@gmail.com> writes:
> 
> > I am fooling around with SPARK (I always wanted to learn to use it)
> > and I want to put the "main" procedure (that is in a body file of its
> > own) in SPARK_Mode, but with no success so far.
> >
> > I tried many things including (but not limited to :-))
> >  
> > * Using Pragma SPARK_Mode (with and without "On") at the beginning of
> >   the file
> >
> > * Using Pragma SPARK_MODE after the "is" 
> >
> > * Using 
> >   procedure Main with SPARK_Mode => is ....
> >
> > and other variations that I do not remember.
> >
> > The only way I was able to put the procedure in SPARK mode is by
> > putting it into a package, but in this way it cannot be the "main"
> > (right?).  I solved the problem by having a microscopic main procedure
> > whose only action is to call the true main in the package, but it
> > seems to me less than ideal...
> >
> > Any suggestions?
> 
> I just tried
> 
>    project Spark_Main is
>       for Source_Files use ("spark_main.adb");
>    end Spark_Main;
> 
> and
> 
>    procedure Spark_Main with SPARK_Mode is
>    begin
>       null;
>    end Spark_Main;
> 
> and it worked OK.

I know it sounds crazy, but I am pretty sure I tried this too...

There is maybe a difference... I do not know if it is important, but in my setup the main procedure is a child of a "big root package" (this is a setup that I usually find convenient).  Could this be the difference?  I'll try later.

Re: How to put main procedure in SPARK_Mode?

[Shark8]

On Tuesday, May 21, 2019 at 8:22:37 AM UTC-6, mockturtle wrote:
> On Tuesday, May 21, 2019 at 4:14:44 PM UTC+2, Simon Wright wrote:
> > mockturtle writes:
> > 
> > > I am fooling around with SPARK (I always wanted to learn to use it)
> > > and I want to put the "main" procedure (that is in a body file of its
> > > own) in SPARK_Mode, but with no success so far.
> > >
> > > I tried many things including (but not limited to :-))
> > >  
> > > * Using Pragma SPARK_Mode (with and without "On") at the beginning of
> > >   the file
> > >
> > > * Using Pragma SPARK_MODE after the "is" 
> > >
> > > * Using 
> > >   procedure Main with SPARK_Mode => is ....
> > >
> > > and other variations that I do not remember.
> > >
> > > The only way I was able to put the procedure in SPARK mode is by
> > > putting it into a package, but in this way it cannot be the "main"
> > > (right?).  I solved the problem by having a microscopic main procedure
> > > whose only action is to call the true main in the package, but it
> > > seems to me less than ideal...
> > >
> > > Any suggestions?
> > 
> > I just tried
> > 
> >    project Spark_Main is
> >       for Source_Files use ("spark_main.adb");
> >    end Spark_Main;
> > 
> > and
> > 
> >    procedure Spark_Main with SPARK_Mode is
> >    begin
> >       null;
> >    end Spark_Main;
> > 
> > and it worked OK.
> 
> I know it sounds crazy, but I am pretty sure I tried this too...
> 
> There is maybe a difference... I do not know if it is important, but in my setup the main procedure is a child of a "big root package" (this is a setup that I usually find convenient).  Could this be the difference?  I'll try later.

Hm, you could try the following:

-- whatever.child.pkg.main_program.ads
Procedure whatever.child.pkg.main_program
  with SPARK_Mode => On, Depends => Null;

-- Main.ads
Procedure Main
  with SPARK_Mode => On;

-- Main.adb
With whatever.child.pkg.main_program;
Procedure Main
  renames whatever.child.pkg.main_program;

I *think* this will give you a good SPARK-proven main-program; plus it's good if you have several alternate "main" programs that you want to try out.

Re: How to put main procedure in SPARK_Mode?

[Simon Wright]

mockturtle <framefritti@gmail.com> writes:

> There is maybe a difference... I do not know if it is important, but
> in my setup the main procedure is a child of a "big root package"
> (this is a setup that I usually find convenient).  Could this be the
> difference?  I'll try later.

I think you need a spec for the child main procedure, also 'with SPARK_Mode'.