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 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-12 00:20:47 PST Path: archiver1.google.com!postnews1.google.com!not-for-mail From: rod.chapman@praxis-cs.co.uk (Rod Chapman) Newsgroups: comp.lang.ada Subject: Re: employment with ada Date: 12 May 2003 00:20:47 -0700 Organization: http://groups.google.com/ 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: 213.152.53.239 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Trace: posting.google.com 1052724047 25647 127.0.0.1 (12 May 2003 07:20:47 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: 12 May 2003 07:20:47 GMT Xref: archiver1.google.com comp.lang.ada:37222 Date: 2003-05-12T07:20:47+00:00 List-Id: Hyman Rosen wrote in message news:... > Well, my primary question is how you expect to convince anyone except > for the already converted when you start talking about "a shack built > on a swamp". That quote actually comes from a prominent member of the C community, not from me, and was used with his permission. It is indeed a slightly tongue-in-cheek assessment of the language, and I presented it as such. Perhpas this doesn't come across clearly enough in the slides alone. > The PDFs talk about C ambiguity. What exactly is this supposed to mean, > and why is it a problem? C (like Ada) has plenty of ambiguity in its defintion - to use the Ada terminology, these are the implementation-defined, implementation- dependent and erroneous bit of the langauge. ISO C90 lists about 205 of these I think. > On the other hand, the sample rules for MISRA-C seem to just be rules of > correct C as opposed to limitations on the language. I assume that there > are actually some rules which do impose constraints. Absolutely - some of the rules limit the use of casts and pointer arithmetic, for example, which are very important constraints. > The ASSENT product > pages claim that they have a complete checking environment for all the > rules which can be examined by source, but you seem to doubt that this > can be true without explaining why. Owing to the ambiguity of the definition (both of C and of the MISRA rules), the notion of "compliance" is very hard to pin down. Some of the rules are also require very deep analysis (MISRA rule 30, for example, effectively requires global inter-procedural data-flow analysis which is very hard in the presence of general pointer effects and aliasing.) In the study conducted by Pi Technology, some tools were found to attempt a deep analysis (but are slow) and some tools do a less deep analysis but are faster. Which tool is correct? Which would you buy? :-) > Are there multiple implementations of the SPARK Examiner from different > companies? If not, criticism of multiple MISRA-C examiners for producing > somewhat different results is at least a little disingenuous. SPARK is deliberately and carefully designed so the question "Is this program legal SPARK?" always has a "Yes/No" answer that is decideable in polynomial time. (The latter point is important - trying to solve NP-Hard problems in static analysis is bad news if you want to encourage constructive use of the technology...) So...No - no other company has chosen to compete with us in tool support for SPARK as present. BUT...since SPARK _does_ have an unambiguous defintion, it should be possible for such as diverse implementation to be constructed and for it to give identical results to the existing SPARK Examiner. (Actually - now I think of it - there is such a tool, but it isn't publically available. Still - its existance illustrates the point.) - Rod