From: Adam Beneschan <adam@irvine.com>
Subject: Re: SPARK - runtime checks question
Date: Fri, 19 Jun 2009 11:29:55 -0700 (PDT)
Date: 2009-06-19T11:29:55-07:00 [thread overview]
Message-ID: <7b7f62f6-7218-45c2-b4b6-a3becb8e5be0@w35g2000prg.googlegroups.com> (raw)
In-Reply-To: aeccd921-a631-40eb-a614-343cfb338c07@q14g2000vbn.googlegroups.com
On Jun 19, 9:04 am, Rod Chapman <roderick.chap...@googlemail.com>
wrote:
> > and of course 50% of VCs are undischarged in the final report.
>
> The Examiner, by default, doesn't know the values of Natural'First
> and Natural'Last, since these are implementation-defined.
Ummm... only half right. If Natural'First is implementation-defined,
you're working with a rather bizarre implementation.
-- Adam
next prev parent reply other threads:[~2009-06-19 18:29 UTC|newest]
Thread overview: 8+ messages / expand[flat|nested] mbox.gz Atom feed top
2009-06-19 15:26 SPARK - runtime checks question Maciej Sobczak
2009-06-19 15:31 ` Maciej Sobczak
2009-06-19 16:04 ` Rod Chapman
2009-06-19 18:29 ` Adam Beneschan [this message]
2009-06-19 18:55 ` Rod Chapman
2009-06-19 21:38 ` Maciej Sobczak
2009-06-19 18:33 ` Adam Beneschan
2009-06-19 21:16 ` Maciej Sobczak
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox