Re: Issue with SPARK 2014

[Serge Robyns <serge.robyns@gmail.com>]

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;