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.140.27.135 with SMTP id 7mr6836204qgx.9.1463068063833; Thu, 12 May 2016 08:47:43 -0700 (PDT) X-Received: by 10.157.8.54 with SMTP id 51mr125074oty.13.1463068063688; Thu, 12 May 2016 08:47:43 -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!news.glorb.com!11no4027883qgt.0!news-out.google.com!k10ni406igv.0!nntp.google.com!sq19no5562811igc.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Thu, 12 May 2016 08:47:43 -0700 (PDT) In-Reply-To: <5147eaaf-ca03-4288-8036-4f52c3364950@googlegroups.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=88.97.49.112; posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q NNTP-Posting-Host: 88.97.49.112 References: <5147eaaf-ca03-4288-8036-4f52c3364950@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <2dc1c4a4-ec94-4cdf-95fc-c81f851c6845@googlegroups.com> Subject: Re: Proof of array initialization in SPARK 2014 From: Phil Thornley Injection-Date: Thu, 12 May 2016 15:47:43 +0000 Content-Type: text/plain; charset=UTF-8 Xref: news.eternal-september.org comp.lang.ada:30391 Date: 2016-05-12T08:47:43-07:00 List-Id: 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;