Re: [Spark] Converting Arrays

[rod.chapman@praxis-cs.co.uk (Rod Chapman)]

"Out" mode unconstrained arrays are indeed an interesting part
of SPARK.  They have the rather unusual property of having a value
which is not well-defined in such a body, but having attributes
(i.e. 'First and 'Last) which do have well-defined values.

A common trick in this case is to use a local,
hidden procedure to initialise the out parameter:

package body test is

   procedure To_Fullpath (s : String; path : out Fullpath) is

      procedure Init_Path;
      --# global out Path;
      --# derives Path from ;
      is
        --# hide Init_Path;
      begin
         Path := (others => ASCII.NUL); -- note Ada95 not SPARK!
      end Init_Path; -- Warning 10 expected here - hidden body.

   begin    
      Init_Path;       
      ... -- as before...
   end To_Fullpath;
end test;

This is a fine example of "moving the SPARK boundary" for perfectly
good reasons.  You can even Inline such a local procedure if efficiency
is as issue.
 - Rod, SPARK Team