brian wichmann (Brian.Wichmann(at)freenet.co.uk)
Sun, 03 Mar 2002 18:11:09 +0000
>Hi all, > >There is a fundamental sense in which OO design makes reasoning (e.g., >verification) more difficult than in non-OO designs. That is due to >the dynamic dispatch used in method calls. When one writes a call >such as > > o.m() > >then code used for the method m at run-time depends on the run-time >type of o, as opposed to its static type. Verification is done >statically, however, and so depends on the specifications associated >with the static type of o. Thus in reasoning, you have a fundamental >problem: how to ensure that each of the subtypes of o's static type >behaves according to the specification of o's static type. This is >where the notion of behavioral subtyping is useful. It had always been my assumption that coding standards precluded dynamic dispatching. The Ada Guidelines exclude this, see ISO/TR 15942:2000. Brian.