Issue with SPARK 2014

Issue with SPARK 2014

[Serge Robyns]

I'm trying to use SPARK on a little game, so far only one error remains and I've no clue on how to fix this.  I've been trying various approaches.
Here is the code snippet (hopefully complete enough).

      Count1      : Natural range 0 .. Number_Of_Columns;
      Count2      : Natural range 0 .. Number_Of_Columns;
      J           : 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 <= Integer (Columns'Pred (Column) - Columns'First) );
            exit when The_Board.Board (Row, J) /= Player;
            Count1 := Count1 + 1;
         end loop;
      end if;

Alternative:
      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;

I get similar errors on both:
medium: loop invariant might fail after first iteration, requires Count1 <= Columns'pred - 1
medium: loop invariant might fail after first iteration, requires Count2 < Number_Of_Columns

Re: Issue with SPARK 2014

[joakimds]

Dear Serge,

Please make a compilable example and put the code for example on github. As the code stands now it is not known exactly what Number_Of_Columns and Columns are.

Best regards,
Joakim Strandberg

Re: Issue with SPARK 2014

[Serge Robyns]

On Tuesday, 13 October 2015 23:40:42 UTC+3, joak...@kth.se  wrote:
> Dear Serge,
> 
> Please make a compilable example and put the code for example on github. As the code stands now it is not known exactly what Number_Of_Columns and Columns are.
> 
> Best regards,
> Joakim Strandberg

These are the most important definitions:

   Number_Of_Columns : constant := 7;
   First_Column : constant := 1;
   First_Row : constant := 1;
   Winning_Move : constant := 4;
   Nil_Move : constant := 0;

   type Player_Type is (Nobody, Human, Computer);
   type Board_Type is private;

   subtype Move_Range is Natural range Nil_Move .. Number_Of_Columns;
   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 Moves is new Move_Range;
   type Columns is new Column_Range;
   type Rows is new Row_Range;

Some of these could have been done differently in Ada2012 (but the code dates from 95 days).

Re: Issue with SPARK 2014

[Simon Wright]

Looks as though you might have problems if Number_Of_Columns is 1.

Also, your variable J is hidden by the loop variables J.

Re: Issue with SPARK 2014

[Serge Robyns]

On Wednesday, 14 October 2015 09:16:17 UTC+3, Simon Wright  wrote:
> Looks as though you might have problems if Number_Of_Columns is 1.
> 
> Also, your variable J is hidden by the loop variables J.

I agree it is not clean to have J declared above, but I needed a loop counter for the J part in a while loop in later the same function.  So i don't mind it hidden in the loop.  But that way I can keep a consistent The_Board.Board (I, J)
constructs.

This is how Number_Of_Columns is declared.
   Number_Of_Columns : constant := 7;

I really don't get it.  The code runs fine.  By reading I believe I've put all controls to avoid incorrect loops.  SPARK seems not to agree with me.

Re: Issue with SPARK 2014

[Stuart]

On Tuesday, 13 October 2015 18:37:08 UTC+1, Serge Robyns  wrote:
> I'm trying to use SPARK on a little game, so far only one error remains and I've no clue on how to fix this.  I've been trying various approaches.
> Here is the code snippet (hopefully complete enough).
...
> medium: loop invariant might fail after first iteration, requires Count1 <= Columns'pred - 1
> medium: loop invariant might fail after first iteration, requires Count2 < Number_Of_Columns

It has been a while (and a few versions of SPARK) since I played with this, but I think the problem is that your loop invariants are not strong enough - they don't carry enough information around the loop.

IIRC the loop invariant acts as a cut point, and it is only information in the invariant that is carried around the loop, earlier knowledge derived from the modelling of the code and the pre-conditions is lost (unless it is embedded in the loop invariant).

In your first case the only knowledge carried around the loop is that:
   Count1 was <= Integer (Columns'Pred (Column) - Columns'First)
   and you incremented it.

Consequently, at the next iteration SPARK warns you that the Invariant might fail, because if it was equal to  Integer (Columns'Pred (Column) - Columns'First) before, it will now (because of the increment) be greater!!

Unfortunately I do not have access to a copy of SPARK or the manuals here to help you resolve it (I expect an expert will be along in a while), but I would guess that you need to strengthen the invariant to an equality statement that remains true.

Re: Issue with SPARK 2014

[Phil Thornley]

On Wednesday, 14 October 2015 21:04:52 UTC+1, Stuart  wrote:
> On Tuesday, 13 October 2015 18:37:08 UTC+1, Serge Robyns  wrote:
> > I'm trying to use SPARK on a little game, so far only one error remains and I've no clue on how to fix this.  I've been trying various approaches.
> > Here is the code snippet (hopefully complete enough).
> ...
> > medium: loop invariant might fail after first iteration, requires Count1 <= Columns'pred - 1
> > medium: loop invariant might fail after first iteration, requires Count2 < Number_Of_Columns
> 
> It has been a while (and a few versions of SPARK) since I played with this, but I think the problem is that your loop invariants are not strong enough - they don't carry enough information around the loop.
> 
> IIRC the loop invariant acts as a cut point, and it is only information in the invariant that is carried around the loop, earlier knowledge derived from the modelling of the code and the pre-conditions is lost (unless it is embedded in the loop invariant).
> 
> In your first case the only knowledge carried around the loop is that:
>    Count1 was <= Integer (Columns'Pred (Column) - Columns'First)
>    and you incremented it.
> 
> Consequently, at the next iteration SPARK warns you that the Invariant might fail, because if it was equal to  Integer (Columns'Pred (Column) - Columns'First) before, it will now (because of the increment) be greater!!
> 
> Unfortunately I do not have access to a copy of SPARK or the manuals here to help you resolve it (I expect an expert will be along in a while), but I would guess that you need to strengthen the invariant to an equality statement that remains true.

Stuart's explanation is quite correct.

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.

(and next time put up compilable code).

Cheers,

Phil

Re: Issue with SPARK 2014

[Stuart]

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 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!

Re: Issue with SPARK 2014

[Serge Robyns]

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;

Re: Issue with SPARK 2014

[Phil Thornley]

On Tuesday, 15 October 2015 18:28:39 UTC+1, Serge Robyns  wrote:
[snip]
> 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.

No, the use of constants in the procedure call is irrelevant.

> 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.

That's exactly what is done - the Evaluate_Board procedure is proved for all 
possible (valid) calls.

> 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.

Every loop has a loop invariant (it's needed to cut the code as Stuart 
explained). If you don't supply one the SPARK tools create a default one.

The messages that you get without an explicit loop invariant are because the 
default loop invariant isn't strong enough for this code.

> 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.

[code snipped]

I don't think that you need more than one Loop_Variant in any loop, this is 
only needed to prove termination of the loop and just one valid loop variant 
should be enough.

Cheers,

Phil


---
This email has been checked for viruses by Avast antivirus software.
https://www.avast.com/antivirus


--- news://freenews.netfront.net/ - complaints: news@netfront.net ---

Re: Issue with SPARK 2014

[Serge Robyns]

> 
> The messages that you get without an explicit loop invariant are because the 
> default loop invariant isn't strong enough for this code.

What is missing to make this one stronger?  Looks like missing a point.

> I don't think that you need more than one Loop_Variant in any loop, this is 
> only needed to prove termination of the loop and just one valid loop variant 
> should be enough.
> 

OK, I capture the the point of the variants part.  Looks like wanted to be too verbose.

Regards,
Serge