Re: Preventing type extensions

[Cyrille <comar@eu.adacore.com>]

On Sep 24, 10:39 am, Cyrille <co...@eu.adacore.com> wrote:
> On Sep 24, 10:16 am, "J-P. Rosen" <ro...@adalog.fr> wrote:
>
> > and replace every redispatching call to M2 by a call to M2_Class, then
> > the big case disappears. You need (of course) to check coverage for
> > M2_Class, but M1 needs to be checked only for values of type T, not for
> > descendants. That's what I meant when I said that coverage testing drops
> > from N to 1
>
> OK, I kind of supposed you had something like that in mind. Many years
> ago, we proposed a similar idea in a few papers, See for instancehttp://www.adacore.com/wp-content/uploads/2006/03/Certification_OO_Ad....
> Another one written by Franco G. is even mentioned in Chelinsky's FAA
> study on OO (seehttp://www.tc.faa.gov/its/worldpac/techrpt/ar0717.pdf).
> The study is worth reading by the way... We had more automatic
> translation in mind at the time but the idea is the same.
> doing this

Sorry, I hit the send button inadvertently. I was going to say:

Suggesting to do such a transformation manually at the source code
level as you do is particularly dubious since it is in the category of
program transformations whose only purpose is to circumvent specific
verifications. There are many such transformations that have been
proposed to make MC/DC coverage easier... some would say to cheat on
MC/DC... and, not surprisingly, it is not very well perceived by cert
authorities.

Anyway, DO-178C doesn't impose "pessimistic testing" as the only way
to to verify safety of dispatching calls. It allows you to treat
dispatching calls as normal calls as long as you can show separately
that you have "local type consistency" (read LSP) for the types
involved in dispatching calls. This additional verification can be
done formally or using specifically designed tests such as verifying
that all the functional tests attached to a class also work when the
objects of this class involved in the testing  are substituted by
objects of the subclass.

If your class hierarchy hasn't been designed to respect LSP (or if you
are in a situation where you need to express properties that don't fit
well with LSP, such as the example Dmitry gave earlier) then you have
to go the pessimistic testing road. Why? because if you don't, there
is a real risk that a non-conforming subclass method misbehave on a
given dispatching call and standard coverage criteria doesn't
guarantee that you have covered such case. If you want to use the
"trick" you mention above, you better find a convincing reason at the
design level for such a "peculiar" style because the transformation
you suggest doesn't address the specific vulnerability that is
supposed to be addressed by either pessimistic testing or the
additional local type consitency verification.

To conclude about differentiating T and T'Class, the trick you suggest
here is easily implementable in other OO languages. There is nothing
magic in creating a wrapper around a given dispatching call and use
this wrapper at each dispatch point. The only problem is that it
doesn't address the (perceived) vulnerability and thus doesn't meet
properly the do-178c objective.