Re: Larch/C


We recognized almost from the outset that the C and preprocessor
combination is so general that our abstraction/interface-oriented
specification techniques wouldn't be adequate to specify arbitrary
programs.  We decided to cater to a restricted class of C interfaces.  In
particular, we only specify macros that either define constants or give the
effect of "inlining" the implementation associated with a function

The lclint checker that Dave Evans wrote at MIT looks at the output of the
preprocessor, so this does not limit the freedom of the implementor to use
macros in creative ways within the implementation.  It just means that we
don't provide a way to specify the properties of non-conforming macros as
part of an interface.

As Gary Leavens has pointed out, the specifications themselves aren't
processed by the C preprocessor, so not all the giddy opportunities to hang
yourself are provided by the present system.

Jim H.