comp.lang.ada
 help / color / mirror / Atom feed
From: Bob Duff <bobduff@theworld.com>
Subject: Re: SPARK: missing case value
Date: Fri, 09 Oct 2015 10:53:49 -0400
Date: 2015-10-09T10:53:49-04:00	[thread overview]
Message-ID: <87pp0o9jpe.fsf@theworld.com> (raw)
In-Reply-To: 9c3de690-e770-412e-b78f-4d254694ffcc@googlegroups.com

Mark Lorenzen <mark.lorenzen@gmail.com> writes:

> I think it is logical and correct. How would a compiler be able to determine
> the range of E if your precondition was more complex?

Well, the fact that compilers cannot prove ALL truthful things (see
halting problem ;-)) doesn't mean they shouldn't be required to prove
some simple things.

- Bob

  reply	other threads:[~2015-10-09 14:53 UTC|newest]

Thread overview: 17+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2015-10-09 11:38 SPARK: missing case value Maciej Sobczak
2015-10-09 12:28 ` Stefan.Lucks
2015-10-09 12:35 ` Mark Lorenzen
2015-10-09 14:53   ` Bob Duff [this message]
2015-10-09 14:39 ` Bob Duff
2015-10-09 15:10   ` Dmitry A. Kazakov
2015-10-09 15:22     ` Bob Duff
2015-10-09 15:34       ` Dmitry A. Kazakov
2015-10-09 16:20     ` G.B.
2015-10-09 16:35       ` Dmitry A. Kazakov
2015-10-09 20:29         ` Georg Bauhaus
2015-10-09 21:01           ` Dmitry A. Kazakov
2015-10-10  6:44             ` Randy Brukardt
2015-10-10  9:10             ` Georg Bauhaus
2015-10-10 10:00               ` Dmitry A. Kazakov
2015-10-10 14:19                 ` Georg Bauhaus
2015-10-11  9:49                   ` Dmitry A. Kazakov
replies disabled

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