From: Stefan.Lucks@uni-weimar.de
Subject: Re: SPARK: missing case value
Date: Fri, 9 Oct 2015 14:28:21 +0200
Date: 2015-10-09T14:28:21+02:00 [thread overview]
Message-ID: <alpine.DEB.2.20.1510091408020.23852@debian> (raw)
In-Reply-To: <ad7b2827-9111-4d9b-b065-1ebd26795365@googlegroups.com>
[-- Attachment #1: Type: text/plain, Size: 1745 bytes --]
On Fri, 9 Oct 2015, Maciej Sobczak wrote:
> type Enum is (A, B, C);
>
> procedure Test (E : in Enum)
> with Pre => E /= C
> is
> begin
case Thingsome(Something(E)) is -- this was "case E is"
> when A => null;
> when B => null;
> end case;
> end Test;
with some functions Thingsome and Something (X: Enum) return Enum.
> The Pre contract says that C is never used as a value for E. Still,
> GNATProve complains about missing case value C in the case statement.
> The compiler complains, too.
Well, your example is a triviality to prove.
But if Ada where required to deal with your example, why should it not
also be required to deal with my example?
On the other hand, assume the program is technically correct. I.e., for
all E /= C, the property
Thingsome(Something(E)) /=C
actually holds. Do you really expect the Ada compiler to prove this?
SPARK should prove this, in principle. But, for sufficiently complicated
functions Something and Thingsome, SPARKs success on proving this may
depend on your settings (which theorem provers and how much time for
proving you set). The legality of an Ada program should never depend on
such settings. Everything else would kill portability.
And allowing SPARK to compile formally illegal Ada programs would very
regrettably break the compability between SPARK and Ada -- even if there
acutally where any "pure-SPARK-compilers" at all.
So long
Stefan
-------- I love the taste of Cryptanalysis in the morning! --------
www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany----
next prev parent reply other threads:[~2015-10-09 12:28 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 [this message]
2015-10-09 12:35 ` Mark Lorenzen
2015-10-09 14:53 ` Bob Duff
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