From: Vinzent Hoefler <ada.rocks@jlfencey.com>
Subject: Re: Ariane5 FAQ
Date: Tue, 29 Jul 2003 10:06:05 +0200
Date: 2003-07-29T10:06:05+02:00 [thread overview]
Message-ID: <bg5a1g$l7sjg$1@ID-175126.news.uni-berlin.de> (raw)
In-Reply-To: K9oVa.12850$AO6.11742@nwrdny02.gnilink.net
Hyman Rosen wrote:
>Richard Riehle wrote:
>> I am thinking here of SPARK.
>
>The Ariane 4/5 problem had nothing to do with proving the
>correctness of a program. Had they used SPARK, they would
>have informed the verifier of the presumed limits of the
>input, and the verifier would have happily verified that the
>program was correct.
Yes, that's probably true.
>But if the Ariane 4 code had carried the specification limits
>within it, as DbC, or as SPARK assertions, or as range checks,
>perhaps someone might have noticed that the Ariane 5 failed to
>meet those constraints.
That isn't much different from SPARK where you should justify such
decisions for the verifier. I don't think either method would have
helped, because nobody seemed to look at the requirements at all.
Vinzent.
--
Parents strongly cautioned -- this posting is intended for mature
audiences over 18. It may contain some material that many parents
would not find suitable for children and may include intense violence,
sexual situations, coarse language and suggestive dialogue.
next prev parent reply other threads:[~2003-07-29 8:06 UTC|newest]
Thread overview: 158+ messages / expand[flat|nested] mbox.gz Atom feed top
2003-07-21 2:10 Ariane5 FAQ Alexandre E. Kopilovitch
2003-07-21 14:52 ` Hyman Rosen
2003-07-21 15:54 ` Vinzent Hoefler
2003-07-21 18:01 ` Hyman Rosen
2003-07-21 18:10 ` Vinzent Hoefler
2003-07-21 18:49 ` Hyman Rosen
2003-07-21 19:13 ` Vinzent Hoefler
2003-07-21 19:43 ` Hyman Rosen
2003-07-21 20:46 ` Vinzent Hoefler
2003-07-22 2:04 ` Hyman Rosen
2003-07-22 5:12 ` Robert I. Eachus
2003-07-22 19:09 ` Hyman Rosen
2003-07-22 8:03 ` Leif Roar Moldskred
2003-07-22 9:00 ` Vinzent Hoefler
2003-07-23 0:13 ` Hyman Rosen
2003-07-23 0:31 ` Bobby D. Bryant
2003-07-23 13:53 ` Hyman Rosen
2003-07-24 16:35 ` Richard Riehle
2003-07-25 1:21 ` Alexander Kopilovitch
2003-07-25 4:26 ` Richard Riehle
2003-07-25 12:35 ` Hyman Rosen
2003-07-25 15:47 ` Robert I. Eachus
2003-07-25 16:51 ` Hyman Rosen
2003-07-25 18:44 ` Robert I. Eachus
2003-07-25 21:08 ` Simon Wright
2003-07-26 1:02 ` Robert I. Eachus
2003-07-26 2:44 ` Alexander Kopilovitch
2003-07-27 17:05 ` Hyman Rosen
2003-07-27 22:19 ` Alexander Kopilovitch
2003-07-28 1:17 ` Berend de Boer
2003-07-28 2:39 ` Robert I. Eachus
2003-07-28 3:16 ` Hyman Rosen
2003-07-28 17:34 ` Mike Silva
2003-07-28 18:03 ` Hyman Rosen
2003-07-29 0:41 ` Alexander Kopilovitch
2003-07-29 16:24 ` Robert I. Eachus
2003-07-30 0:53 ` Alexander Kopilovitch
2003-07-31 21:41 ` Robert I. Eachus
2003-08-01 20:19 ` Alexander Kopilovitch
2003-07-29 4:43 ` Richard Riehle
2003-07-29 6:06 ` Hyman Rosen
2003-07-29 8:06 ` Vinzent Hoefler [this message]
2003-07-29 19:42 ` Berend de Boer
2003-07-29 21:14 ` Robert I. Eachus
2003-07-30 1:13 ` Berend de Boer
2003-07-30 12:58 ` Richard Riehle
2003-07-30 15:04 ` Hyman Rosen
2003-07-29 19:46 ` Berend de Boer
2003-07-30 6:19 ` Richard Riehle
2003-07-30 7:31 ` Hyman Rosen
2003-07-30 13:03 ` Richard Riehle
2003-07-30 13:16 ` Vinzent Hoefler
2003-07-30 15:06 ` Hyman Rosen
2003-07-30 15:15 ` Vinzent Hoefler
2003-07-30 16:46 ` Hyman Rosen
2003-07-30 16:54 ` Vinzent Hoefler
2003-07-31 8:28 ` Dmitry A. Kazakov
2003-07-31 9:36 ` Vinzent Hoefler
2003-07-31 16:28 ` Warren W. Gay VE3WWG
2003-07-29 19:34 ` Berend de Boer
2003-07-29 20:49 ` Simon Wright
2003-07-29 21:52 ` Robert I. Eachus
2003-07-28 18:01 ` Non-philosophical definition of Eiffel? (was: Re: Ariane5 FAQ) Alexander Kopilovitch
2003-07-28 18:18 ` Non-philosophical definition of Eiffel? Hyman Rosen
2003-07-29 8:43 ` Dmitry A. Kazakov
2003-07-29 13:43 ` Hyman Rosen
2003-07-29 14:56 ` Dmitry A. Kazakov
2003-07-29 16:35 ` Hyman Rosen
2003-07-29 21:39 ` Jim Rogers
2003-07-29 22:33 ` Hyman Rosen
2003-07-30 8:48 ` Pascal Obry
2003-07-30 15:19 ` Hyman Rosen
2003-07-30 18:47 ` Frank J. Lhota
2003-07-30 19:24 ` Hyman Rosen
2003-08-04 18:15 ` Robert Spooner
2003-07-29 22:02 ` Matthew Woodcraft
2003-07-30 9:19 ` Dmitry A. Kazakov
2003-07-30 16:38 ` Hyman Rosen
2003-07-31 9:58 ` Dmitry A. Kazakov
2003-07-31 15:49 ` Hyman Rosen
2003-08-01 7:57 ` Dmitry A. Kazakov
2003-08-01 13:31 ` Hyman Rosen
2003-07-29 19:58 ` Berend de Boer
2003-07-29 20:33 ` Hyman Rosen
2003-07-30 1:20 ` Berend de Boer
2003-07-30 1:49 ` Hyman Rosen
2003-07-30 2:52 ` Berend de Boer
2003-07-30 4:33 ` Hyman Rosen
2003-07-30 4:40 ` Hyman Rosen
2003-07-30 13:16 ` Matthew Heaney
2003-07-30 20:08 ` Berend de Boer
2003-07-30 3:03 ` Berend de Boer
2003-07-30 4:31 ` Hyman Rosen
2003-07-30 20:20 ` Berend de Boer
2003-07-30 21:05 ` Hyman Rosen
2003-07-29 19:51 ` Berend de Boer
2003-07-28 2:11 ` Ariane5 FAQ Hyman Rosen
2003-07-25 17:39 ` Mike Silva
2003-07-25 21:53 ` John R. Strohm
2003-07-22 18:29 ` Mike Silva
2003-07-22 18:50 ` Hyman Rosen
2003-07-22 19:00 ` Bobby D. Bryant
2003-07-22 20:47 ` Mike Silva
2003-07-22 21:11 ` Hyman Rosen
2003-07-22 21:38 ` Bobby D. Bryant
2003-07-23 13:56 ` Hyman Rosen
2003-07-22 21:52 ` Larry Elmore
2003-07-23 14:11 ` Hyman Rosen
2003-07-23 15:08 ` Vinzent Hoefler
2003-07-23 17:48 ` Hyman Rosen
2003-07-23 18:42 ` Robert I. Eachus
2003-07-23 20:18 ` Hyman Rosen
2003-07-23 22:58 ` Robert I. Eachus
2003-07-24 1:42 ` Hyman Rosen
2003-07-24 5:24 ` Mike Silva
2003-07-24 9:57 ` Vinzent Hoefler
2003-07-24 13:52 ` Hyman Rosen
2003-07-24 15:00 ` Vinzent Hoefler
2003-07-23 20:33 ` Mike Silva
2003-07-23 21:35 ` Hyman Rosen
2003-07-23 23:10 ` Robert I. Eachus
2003-07-24 5:16 ` Mike Silva
2003-07-22 4:57 ` Richard Riehle
2003-07-22 9:00 ` Vinzent Hoefler
2003-07-22 9:03 ` John McCabe
2003-07-22 12:28 ` Marin David Condic
2003-07-23 19:40 ` Simon Wright
2003-07-22 3:11 ` Robert I. Eachus
2003-07-22 9:05 ` John McCabe
2003-07-22 9:38 ` Bobby D. Bryant
2003-07-22 16:38 ` Robert I. Eachus
2003-07-21 22:03 ` Bobby D. Bryant
2003-07-22 1:57 ` Hyman Rosen
2003-07-21 18:56 ` Francisco Malpartida
2003-07-22 2:22 ` Hyman Rosen
2003-07-22 7:19 ` Tarjei T. Jensen
2003-07-22 19:06 ` Hyman Rosen
2003-07-22 21:24 ` Robert I. Eachus
2003-07-23 11:55 ` Tarjei T. Jensen
2003-07-23 19:24 ` Robert I. Eachus
2003-07-24 0:36 ` Bobby D. Bryant
2003-07-21 22:00 ` Bobby D. Bryant
2003-07-22 1:59 ` Hyman Rosen
2003-07-22 9:07 ` John McCabe
2003-07-22 13:25 ` Hyman Rosen
2003-07-22 0:16 ` Alexander Kopilovitch
2003-07-22 1:45 ` Hyman Rosen
2003-07-22 7:21 ` Tarjei T. Jensen
2003-07-21 23:24 ` Alexander Kopilovitch
2003-07-22 1:53 ` Hyman Rosen
2003-07-22 16:35 ` Robert I. Eachus
2003-07-22 18:36 ` Mike Silva
2003-07-22 19:23 ` Hyman Rosen
2003-07-22 21:50 ` Robert I. Eachus
2003-07-23 14:21 ` Hyman Rosen
2003-07-23 19:56 ` Robert I. Eachus
2003-07-23 20:26 ` Hyman Rosen
2003-07-23 23:14 ` Robert I. Eachus
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox