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.67.7.35 with SMTP id cz3mr6103224pad.40.1444757826902;
        Tue, 13 Oct 2015 10:37:06 -0700 (PDT)
X-Received: by 10.182.44.163 with SMTP id f3mr187259obm.7.1444757826858; Tue,
 13 Oct 2015 10:37:06 -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!kq10no20855497igb.0!news-out.google.com!n2ni29199igy.0!nntp.google.com!kq10no18264572igb.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Tue, 13 Oct 2015 10:37:06 -0700 (PDT)
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
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <c4a5963b-78eb-4b55-83f5-a1de6b10717d@googlegroups.com>
Subject: Issue with SPARK 2014
From: Serge Robyns <serge.robyns@gmail.com>
Injection-Date: Tue, 13 Oct 2015 17:37:06 +0000
Content-Type: text/plain; charset=ISO-8859-1
Xref: news.eternal-september.org comp.lang.ada:27966
Date: 2015-10-13T10:37:06-07:00
List-Id: <comp.lang.ada>

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