Re: inventing the wheel?

[Werner Almesberger <wa@almesberger.net>]

Carl-Daniel Hailfinger wrote:
> Now we only need one additional tool to *prove* correctness of the
> kernel ;-)

Perhaps another interesting approach for such source code analyzers
would be to take a top-down view, i.e. assume a certain functional
structure, and check that all the elements are there and in the
right order.

This should be feasible for code that basically follows a certain
template, e.g. network card drivers.

This would also help with the update problem of "fill in the blanks"
type of templates, i.e. if the template changes or is augmented,
some drivers using it may no longer conform to it.

Such a top-down view could be layered on top of a bottom-up analyzer,
e.g. by - manually or automatically - translating some "skeleton"
into a set of rules of the type "if you've called X, you must later
call Y", etc.

- Werner

-- 
  _________________________________________________________________________
 / Werner Almesberger, Buenos Aires, Argentina         wa@almesberger.net /
/_http://www.almesberger.net/____________________________________________/