From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,3d6589e7b2c60444 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-05-10 13:35:06 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!logbridge.uoregon.edu!msunews!not-for-mail From: "Chad R. Meiners" Newsgroups: comp.lang.ada Subject: Re: employment with ada Date: Sat, 10 May 2003 16:29:02 -0400 Organization: Michigan State University Message-ID: References: <626e8ae.0305011636.5e899da3@posting.google.com> <4mo7bvc2n70k6eikm3muu2965nbo3m77ov@4ax.com> <3EB415CB.6D97B14D@adaworks.com> <6Mcta.37135$D%4.20715@nwrdny03.gnilink.net> NNTP-Posting-Host: arctic.cse.msu.edu X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2800.1158 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1165 Xref: archiver1.google.com comp.lang.ada:37161 Date: 2003-05-10T16:29:02-04:00 List-Id: "Hyman Rosen" 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