How to put main procedure in SPARK_Mode?

[mockturtle <framefritti@gmail.com>]

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