From: Alexandre K <alexandre.nospam@gmail.com>
Subject: Re: Strategies with SPARK which does not support exceptions
Date: Mon, 21 Jun 2010 07:10:34 -0700 (PDT)
Date: 2010-06-21T07:10:34-07:00 [thread overview]
Message-ID: <6236693f-0658-498d-a3c9-b8f3aea7a856@c10g2000yqi.googlegroups.com> (raw)
In-Reply-To: Xns9D9E60DC6F348WarrensBlatherings@188.40.43.230
> Does SPARK even permit exceptions? I'm too lazy to
> look it up.
>
> Warren
Hi Warren,
Spark doesn't permit exception.
The program that checks your code will complain about it. We can "use"
exception in a
package that is hidden for Spark (so not parsed by the Examiner), but
as it is hidden, we can't proove this body part.
It is the case when you need to call an existing program that is not a
Spark one (Ada.Text_IO ...).
Alex
next prev parent reply other threads:[~2010-06-21 14:10 UTC|newest]
Thread overview: 22+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-06-17 15:33 Strategies with SPARK which does not support exceptions Yannick Duchêne (Hibou57)
2010-06-17 17:11 ` Warren
2010-06-17 18:19 ` Yannick Duchêne (Hibou57)
2010-06-21 13:31 ` Warren
2010-06-21 14:10 ` Alexandre K [this message]
2010-06-17 19:54 ` Pascal Obry
2010-06-17 22:47 ` Peter C. Chapin
2010-06-18 6:07 ` Claude
2010-06-18 8:06 ` Phil Thornley
2010-06-18 8:49 ` Martin
2010-06-18 17:16 ` mockturtle
2010-06-18 21:51 ` Alexandre K
2010-06-22 17:01 ` Phil Clayton
2010-06-22 23:14 ` Claude
2010-06-23 16:22 ` Warren
2010-06-24 3:24 ` Claude
2010-06-28 13:14 ` Warren
2010-06-29 8:39 ` Stephen Leake
2010-06-29 20:05 ` Randy Brukardt
2010-06-29 20:49 ` Georg Bauhaus
2010-06-30 5:08 ` Simon Wright
2010-06-30 8:17 ` stefan-lucks
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox