Re: Proof of array initialization in SPARK 2014

[Phil Thornley <phil.jpthornley@gmail.com>]

On Thursday, May 12, 2016 at 1:01:19 PM UTC+1, Dmitrij Novikov wrote:
> Hi,
> 
> I don't know how to cope with complex array initializations in SPARK.
> 
> When I write:
> 
>   type My_Array is array ( Positive range <> ) of Boolean;
> 
>   function Initialize return My_Array
>   is
>     A : My_Array(1..8); 
>   begin
> 
>     A(A'Last) := False;
> 
>     for I in A'First .. A'Last - 1 loop
>       A(I) := True;
>     end loop;
> 
>     return A;
>   end Initialize;
> 
> The SPARK Examiner gives the warning that 'A' might not be initialized.
> So I tried:
> 
>   type Extended_Boolean is (Uninitialized, False, True);
>   type My_Array is array ( Positive range <> ) of Extended_Boolean;
>   
>   function Initialize return My_Array
>   is
>     A : My_Array(1..8) := (others => Uninitialized);
>   begin
> 
>     A(A'Last) := False;
> 
>     for I in A'First .. A'Last - 1 loop
>       A(I) := True;
>       pragma Loop_Invariant (for all X in A'First .. I => A(X) = True);
>       pragma Loop_Invariant (A(A'Last) = False);
>     end loop;
> 
>     pragma Assert( for all X in A'Range => A(X) /= Uninitialized );
>     
>     return A;
>   end Initialize;
> 
> The initialization can be proven by the theorem prover. But I have a 
> state of my type and an assignment which are only useful for proof and
> useless in the executable. 
> So I can go back to my first version and add:
>  
>   pragma Annotate (GNATprove, False_Positive,
>                      " might not be initialized",
>                     "Initialization proven in separate file");
>                     
> When there would be something like ghost states for variables and ghost 
> assignments I could take the second version and write:
> 
>   type Boolean is (False, True) with Ghost_State => Uninitialized;
>   
> and then:
>   
>   A : My_Array(1..8) := (others => Uninitialized)
>    with Ghost_Assignment => True;
> 
> Are there similar constructs in SPARK 2014 ?
> Or is there a better way to cope with array initialization?

You could use a parallel Ghost array recording the initializations:

   function Initialize return My_Array
   is
      A : My_Array(1..8); 
      A_Is_Init : My_Array(1..8) := (others => False) with Ghost;
   begin

      A(A'Last) := False;
      A_Is_Init(A'Last) := True;

      for I in A'First .. A'Last - 1 loop
         A(I) := True;
         A_Is_Init(I) := True;
         pragma Loop_Invariant (for all J in A'First .. I => A_Is_Init(J));
         pragma Loop_Invariant (A_Is_Init(A'Last));
      end loop;

      pragma Assert (for all J in A'First .. A'Last => A_Is_Init(J));
      
      return A;
   end Initialize;