From: "Chad R. Meiners" <crmeiners@hotmail.com>
Subject: Re: employment with ada
Date: Sat, 10 May 2003 16:29:02 -0400
Date: 2003-05-10T16:29:02-04:00 [thread overview]
Message-ID: <b9jnop$1dn1$1@msunews.cl.msu.edu> (raw)
In-Reply-To: 6Mcta.37135$D%4.20715@nwrdny03.gnilink.net
"Hyman Rosen" <hyrosen@mail.com> wrote in message
news:6Mcta.37135$D%4.20715@nwrdny03.gnilink.net...
> Richard Riehle wrote:
> > Instead, they cobble together a set of restrictions for C
>
> How is this different from SPARK?
SPARK is an excellent (my opinion, I am not affiliated with Praxis) language
that allows you to practice a correctness by construction methodology which
is backed up by powerful proof techniques. In SPARK's case the restrictions
are helpful since they make the proofs more tractable. If you read through
the SPARK rational it will explain why almost every restriction is in place.
So when asking how this differs from a restricted subset of C, I would
speculate that the restricted C is MISRA-C. Praxis appears to have some
information on the differences between SPARK and MISRA-C at
http://www.sparkada.com/assent.html
next prev parent reply other threads:[~2003-05-10 20:29 UTC|newest]
Thread overview: 80+ messages / expand[flat|nested] mbox.gz Atom feed top
2003-05-02 0:36 employment with ada tom
2003-05-02 0:41 ` Ed Falis
2003-05-02 8:51 ` John McCabe
2003-05-02 12:08 ` Marin David Condic
2003-05-02 20:54 ` Bill Sheehan
2003-05-03 3:23 ` R. Srinivasan
2003-05-03 4:13 ` John R. Strohm
2003-05-03 5:03 ` anisimkov
2003-05-03 7:07 ` Anders Wirzenius
2003-05-03 7:46 ` AG
2003-05-05 5:38 ` Anders Wirzenius
2003-05-03 14:44 ` Marin David Condic
2003-05-04 15:32 ` Mark Lorenzen
2003-05-05 11:47 ` Marin David Condic
2003-05-03 14:37 ` Marin David Condic
2003-05-03 16:03 ` DPH
2003-05-03 16:22 ` Chad R. Meiners
2003-05-03 17:18 ` DPH
2003-05-03 20:30 ` Jeffrey Carter
2003-05-03 19:17 ` Richard Riehle
2003-05-03 20:35 ` Jeffrey Carter
2003-05-04 11:01 ` Simon Wright
2003-05-05 0:34 ` Richard Riehle
2003-05-05 2:28 ` Jeffrey Carter
2003-05-05 3:33 ` Wesley Groleau
2003-05-05 12:30 ` Robert A Duff
2003-05-04 13:14 ` DPH
2003-05-05 1:20 ` Richard Riehle
2003-05-07 12:20 ` Marin David Condic
2003-05-08 18:20 ` tmoran
2003-05-09 11:45 ` Marin David Condic
2003-05-09 13:11 ` Hyman Rosen
2003-05-09 17:13 ` Larry Kilgallen
2003-05-05 3:28 ` Wesley Groleau
2003-05-05 10:45 ` DPH
2003-05-05 12:47 ` Ed Falis
2003-05-05 20:19 ` DPH
2003-05-05 20:28 ` Ed Falis
2003-05-06 11:30 ` Marin David Condic
2003-05-07 13:22 ` Stephen Leake
2003-05-08 12:21 ` Marin David Condic
2003-05-05 17:12 ` Simon Wright
2003-05-04 13:20 ` Marin David Condic
2003-05-05 17:19 ` Simon Wright
2003-05-06 12:07 ` Marin David Condic
2003-05-04 18:14 ` Hyman Rosen
2003-05-05 1:24 ` Richard Riehle
2003-05-05 1:27 ` Richard Riehle
2003-05-10 20:29 ` Chad R. Meiners [this message]
2003-05-11 3:32 ` Hyman Rosen
2003-05-11 4:25 ` Chad R. Meiners
2003-05-11 16:43 ` Hyman Rosen
2003-05-11 23:04 ` Chad R. Meiners
2003-05-11 15:29 ` Robert A Duff
2003-05-11 17:14 ` Hyman Rosen
2003-05-11 19:24 ` Rod Chapman
2003-05-11 20:03 ` Hyman Rosen
2003-05-12 7:20 ` Rod Chapman
2003-05-04 0:25 ` John R. Strohm
2003-05-04 4:09 ` DPH
2003-05-04 19:37 ` P S Norby
2003-05-04 4:55 ` Steve
2003-05-04 12:55 ` DPH
2003-05-05 6:27 ` Anders Wirzenius
2003-05-04 12:57 ` Marin David Condic
2003-05-04 16:45 ` tmoran
2003-05-04 13:45 ` Alex Gibson
2003-05-05 4:07 ` William J. Thomsa
2003-05-05 18:41 ` P S Norby
2003-05-05 20:26 ` DPH
2003-05-05 23:06 ` William J. Thomsa
2003-05-05 23:20 ` DPH
2003-05-06 9:24 ` Ole-Hjalmar Kristensen
2003-05-07 1:25 ` Wesley Groleau
2003-05-07 13:23 ` Stephen Leake
2003-05-07 16:36 ` Wesley Groleau
2003-05-06 9:32 ` Preben Randhol
-- strict thread matches above, loose matches on Subject: below --
2003-05-04 1:32 Alexandre E. Kopilovitch
2003-05-06 16:19 ` L. Siever
2003-05-07 13:35 ` Stephen Leake
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox