From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.66.166.166 with SMTP id zh6mr6070651pab.28.1463054478907;
        Thu, 12 May 2016 05:01:18 -0700 (PDT)
X-Received: by 10.157.8.244 with SMTP id 107mr104253otf.0.1463054478862; Thu,
 12 May 2016 05:01:18 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!au2pb.net!feeder.erje.net!2.us.feeder.erje.net!news.glorb.com!sq19no5534634igc.0!news-out.google.com!l67ni590ith.0!nntp.google.com!i5no7868738ige.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Thu, 12 May 2016 05:01:18 -0700 (PDT)
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=193.175.38.9;
 posting-account=lHhhngoAAACPtCnjxceEI7ThHhjTh2oB
NNTP-Posting-Host: 193.175.38.9
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <5147eaaf-ca03-4288-8036-4f52c3364950@googlegroups.com>
Subject: Proof of array initialization in SPARK 2014
From: Dmitrij Novikov <drr73@gmx.de>
Injection-Date: Thu, 12 May 2016 12:01:18 +0000
Content-Type: text/plain; charset=UTF-8
Xref: news.eternal-september.org comp.lang.ada:30387
Date: 2016-05-12T05:01:18-07:00
List-Id: <comp.lang.ada>

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?