From: Phil Thornley <phil.jpthornley@gmail.com>
Subject: Re: Question about out parameters of unconstrained array type.
Date: Mon, 27 Feb 2012 15:32:57 -0000
Date: 2012-02-27T15:32:57+00:00 [thread overview]
Message-ID: <MPG.29b5b16ea55019b398968d@news.zen.co.uk> (raw)
In-Reply-To: 4e2c786f-8485-436f-b9c5-c8c19cf00805@q12g2000yqg.googlegroups.com
In article <4e2c786f-8485-436f-b9c5-c8c19cf00805
@q12g2000yqg.googlegroups.com>, mark.lorenzen@gmail.com says...
>
> On 25 Feb., 23:44, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
> > > Would SPARK accept
> >
> > > ᅵ ᅵfor I in S'Range loop
> >
> > > ?
> >
> > No - the subtype of the loop index is still regarded as anonymous.
>
> Phil
>
> Do you know the rationale for this? Why can't the examiner just
> generate hypotheses like
>
> loop__1__i <= s__index__subtype__1__last
> loop__1__i >= s__index__subtype__1__first
>
> and then generate appropriate hypotheses regarding
> s__index__subtype__1__last and s__index__subtype__1__first?
Mark,
I don't know of any specific reasoning, but the rule that an explicit
subtype mark must be given is a fundamental rule in the grammar, so I
guess there would have to be a very substantial gain from modifying it
before such a change was considered.
Cheers,
Phil
next prev parent reply other threads:[~2012-02-27 15:32 UTC|newest]
Thread overview: 15+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-02-25 15:19 Question about out parameters of unconstrained array type Peter C. Chapin
2012-02-25 15:33 ` Dmitry A. Kazakov
2012-02-25 18:20 ` Phil Thornley
2012-02-25 20:01 ` Simon Wright
2012-02-25 22:44 ` Phil Thornley
2012-02-27 13:48 ` Mark Lorenzen
2012-02-27 15:32 ` Phil Thornley [this message]
2012-02-25 23:37 ` Alexander Senier
2012-02-26 1:16 ` Peter C. Chapin
2012-02-26 9:14 ` Phil Thornley
2012-02-26 12:25 ` Alexander Senier
2012-02-26 13:20 ` Phil Thornley
2012-02-26 14:25 ` Niklas Holsti
2012-02-26 17:32 ` Jeffrey Carter
2012-02-26 15:29 ` Peter C. Chapin
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox