Re: Required Metrics

[Robert Dewar <robert_dewar@my-deja.com>]

In article <%MoQ4.7915$wb7.556168@news.flash.net>,
  "Ken Garlington" <Ken.Garlington@computer.org> wrote:

> > For a validated compiler -- difficult! In particular, how
> > can the DOC be signed if you have ignored a requirement.
>
> I suspect with a pen in the hand, and a song in the heart!

Ken, do you think it is fair to accuse vendors of dishonesty
and duplicity with no evidence at all to back up your
statements. I will say right away that I personally sign
all DOC's for Ada Core Technologies, and in all cases I
do so with integrity knowing that what I am signing is
absolutely correct. I would assume that all other vendors
would make the same statement.

> I think you read the statement backwards, by the way. To
> repeat: The issue
> isn't, in my mind, "How easy is it for vendors to ignore
> certain
> requirements?".  It's "Is there really a requirement?"

For the case of documentation requirements, the answer is
basically no, it is not a requirement at all in the usual
formal semantic sense.

> > Once again, the documentation requirements, the primary
subject
> > of this thread, are in a rather special category, since
these
> > are untestable, undefined requirements. Normally one would
not
> > expect to find untestable, undefined stuff in a language
> > standard, and for the most part, one does not in the Ada RM,
> > but I am afraid there are exceptions :-)

> I suspect, after you read the discussion of pragma Reviewable,
we're going
> to be expanding this to "documentation and some implementation
requirements"

  Nope, the issues with pragma Reviewable are also all
  documentation based, let's look:

  The definition of pragma reviewable is in two sections
  BOTH of them have the language:

    THe implementation shall provide the following
    information ....

Well, "shall" is an impressive word, it sure *sounds* like
a requirement. Unfortunately, what on earth does it mean to
"provide the following information". Ooops, totally undefined.
And since the information for ALL sections is equivalent to
information provided in the object file, you can argue from
a formal point of view that the object file satisfies the
requirement.

Now of course from a pragmatic point of view, we want the
information in a much more usable form, and GNAT provides
a lot of *non-required* capabilities in this area. For
example, let's take:

    6  Where compiler-generated run-time checks remain;

From a formal point of view, we could just say "look in the
object module for all calls to __gnat_raise_constraint_error
or whatever, but in practice it is useful (but not required)
to have this information in a clearer source-related fashion.
So GNAT provides the generated source listing, where for
example if you write

    x := a(b,c);

in the source, then the generated source listing (-gnatG) might
say:

    x := a(b,{c});

where, as documented in the GNAT documentation, the curly
brackets mean that the expression inside is range checked
at run time.

That's a nice feature, very useful for users, and definitely
meeting the spirit of the requirement quoted above.

But in a formal language definition, we are not in the business
of meeting the spirit of requirements!

It would have been SO much better to make all these
documentation "requirements" into implementation advice
for several reasons:

 1. In IA sections, since they are not part of the formal
    standard, we are much freer to make informal requirements
    of the "you-will-know-it-when-you-see-it" form.

 2. IA sections get interpreted in a pragmatic manner, which
    is just right for this purpose.

 3. Implementors have to document which IA they follow and
    which they do not, leading to a useful account of how
    each IA section is addressed (see the section in the
    GNAT RM that does this for example).








Sent via Deja.com http://www.deja.com/
Before you buy.