comp.lang.ada
 help / color / mirror / Atom feed
From: Serge Robyns <serge.robyns@gmail.com>
Subject: Re: Issue with SPARK 2014
Date: Wed, 14 Oct 2015 08:23:57 -0700 (PDT)
Date: 2015-10-14T08:23:57-07:00	[thread overview]
Message-ID: <128844c2-2f5d-4d91-a267-7f7e05c8ca86@googlegroups.com> (raw)
In-Reply-To: <lyeggyvuts.fsf@pushface.org>

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.

  reply	other threads:[~2015-10-14 15:23 UTC|newest]

Thread overview: 11+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2015-10-13 17:37 Issue with SPARK 2014 Serge Robyns
2015-10-13 20:40 ` joakimds
2015-10-14 15:25   ` Serge Robyns
2015-10-14  6:16 ` Simon Wright
2015-10-14 15:23   ` Serge Robyns [this message]
2015-10-14 20:04 ` Stuart
2015-10-15  8:44   ` Phil Thornley
2015-10-15 11:23     ` Stuart
2015-10-15 17:28       ` Serge Robyns
2015-10-18  8:44         ` Phil Thornley
2015-10-19  9:13           ` Serge Robyns
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox