Re: employment with ada

[rod.chapman@praxis-cs.co.uk (Rod Chapman)]

Hyman Rosen <hyrosen@mail.com> wrote in message news:<E0yva.16125$rV2.12620@nwrdny01.gnilink.net>...

> 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