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.182.24.42 with SMTP id r10mr8391334obf.42.1444930119329; Thu, 15 Oct 2015 10:28:39 -0700 (PDT) X-Received: by 10.182.248.230 with SMTP id yp6mr114695obc.20.1444930119304; Thu, 15 Oct 2015 10:28:39 -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!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!peer03.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!border1.nntp.dca1.giganews.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!kq10no21745962igb.0!news-out.google.com!z4ni21912ign.0!nntp.google.com!kq10no18836484igb.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Thu, 15 Oct 2015 10:28:39 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=197.248.28.186; posting-account=6m7axgkAAADBKh082FfZLdYsJ24CXYi5 NNTP-Posting-Host: 197.248.28.186 References: <4187f92b-770a-4d76-85c0-14f2eba2dee8@googlegroups.com> <41a7f7f9-65b4-43a3-b817-f5d9c6a3d015@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: Issue with SPARK 2014 From: Serge Robyns Injection-Date: Thu, 15 Oct 2015 17:28:39 +0000 Content-Type: text/plain; charset=ISO-8859-1 X-Received-Bytes: 5170 X-Received-Body-CRC: 3077464802 Xref: news.eternal-september.org comp.lang.ada:27987 Date: 2015-10-15T10:28:39-07:00 List-Id: On Thursday, 15 October 2015 14:23:41 UTC+3, Stuart wrote: > On Thursday, 15 October 2015 09:44:39 UTC+1, Phil Thornley wrote: > ... > > Stuart's explanation is quite correct. > [Thank you :-)] > > > In the first version try changing the bound on Count1 to: > > Integer (Columns'Pred (Column) - J) > > so that it starts at 0 and increments by 1 on each loop. > ... > Having thought about it a bit more (but still no opportunity to test) I thought that example 1 could use the invariant: > Count1 = Integer(J-Columns'First) > This one makes it even worse .... > This seems to capture the essence of the loop (always a good sign for a loop invariant) > > In the absence of the full code getting a definitive useful loop invariant is not possible! When trying to build a small standalone body I gets proved successfully with the below code. However the call is using constant values. I'm wondering if the fact that here the prover has constants in the procedure call makes it possible for him to prove it. Now in essence the moves are either given by a player or selected by an algorithm. I was expecting that SPARK could prove the procedure by using the procedure signature, in worst case pre/post conditions. The essence I'm trying to state in the loop invariant (which I've put to shut up other SPARK messages) is that the count will never exceed a certain range. You can't have more "tiles" than there is space to put them. Now I play with this code from time to time when I've an urge to make it proven or when I read about how nice spark is. procedure Four with SPARK_Mode is Number_Of_Columns : constant := 7; First_Row : constant := 1; First_Column : constant := 1; Winning_Move : constant := 4; type Player_Type is (Nobody, Human, Computer); type Valid_Move_Range is range First_Column .. Number_Of_Columns; subtype Column_Range is Valid_Move_Range; subtype Row_Range is Valid_Move_Range; type Columns is new Column_Range; type Rows is new Row_Range; type Board_Array is array (Rows, Columns) of Player_Type; type Board_Type is record Score : Integer := 0; Winning : Boolean := False; Board : Board_Array := (others => (others => Nobody)); end record; My_Board : Board_Type; procedure Evaluate_Board (The_Board : in out Board_Type; Player : in Player_Type; Row : in Rows; Column : in Columns) is Count1 : Natural range 0 .. Number_Of_Columns; Count2 : Natural range 0 .. Number_Of_Columns; begin Count1 := 0; if Column > Columns'First then for J in reverse Columns'First .. Columns'Pred (Column) loop pragma Loop_Variant ( Increases => Count1 ); pragma Loop_Variant ( Decreases => J ); pragma Loop_Invariant ( Count1 < Number_Of_Columns ); exit when The_Board.Board (Row, J) /= Player; Count1 := Count1 + 1; end loop; end if; Count2 := 0; if Column < Columns'Last then for J in Columns'Succ (Column) .. Columns'Last loop pragma Loop_Variant ( Increases => Count2 ); pragma Loop_Variant ( Increases => J ); pragma Loop_Invariant ( Count2 < Number_Of_Columns ); exit when The_Board.Board (Row, J) /= Player; Count2 := Count2 + 1; end loop; end if; -- The_Score := The_Score + Evaluate_Score (Count1, Count2); if Count1 + Count2 + 1 >= Winning_Move then The_Board.Winning := true; end if; end Evaluate_Board; begin Evaluate_Board (My_Board, Computer, 7, 2); end Four;