From: Simon Wright <simon@pushface.org>
Subject: Re: ANNOUNCE: SPARK toolset 6.1 now available
Date: 13 Jul 2002 19:11:20 +0100
Date: 2002-07-13T19:11:20+01:00 [thread overview]
Message-ID: <x7vznwvjy5z.fsf@pushface.org> (raw)
In-Reply-To: wccwurzzpb7.fsf@shell01.TheWorld.com
Robert A Duff <bobduff@shell01.TheWorld.com> writes:
> Simon Wright <simon@pushface.org> writes:
>
> > I would be _very_ surprised if SPARKada allowed T'Class
> > (uncertainty being something you don't want in safety-related
> > software).
>
> If you have the entire program source code (which you should in a
> safety-critical context), then I don't see why a dispatching call is
> any more "uncertain" than a case statement.
I don't want to put words into Praxis's mouths, as it were, but a case
statement is very localised and less hard to reason about than a
dispatching call over an extended space.
Some of the reasoning for the position is probably practical: if you
have proof obligations to discharge and you can get machine help in
the proving, but only if you avoid Feature X (because -- for whatever
reason -- the tool doesn't do it), you probably will avoid Feature X
because the pain of doing the proof by hand is so much greater!
next prev parent reply other threads:[~2002-07-13 18:11 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2002-07-11 7:57 ANNOUNCE: SPARK toolset 6.1 now available Rod Chapman
2002-07-11 14:04 ` Ted Dennison
2002-07-12 8:52 ` Rod Chapman
2002-07-12 20:14 ` Randy Brukardt
2002-07-13 13:37 ` Simon Wright
2002-07-13 14:15 ` Robert A Duff
2002-07-13 18:11 ` Simon Wright [this message]
2002-07-13 20:15 ` Rod Chapman
2002-07-14 0:27 ` Randy Brukardt
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox