David Guaspari writes:

   General question about Larch/C:  Actual C programmers don't
   write for the compiler -- they write for the C preprocessor.  So
   the code they read, (purportedly) understand, and maintain
   doesn't necessarily look like anything that could even be
   annotated in Larch/C.

We have thought some about allowing the Larch/C++ user to specify macros.
But at the moment we haven't gotten very far with it.

   I'll just note the giddy possibility that one could allow
   the preprocessor to cobble together not only the code but also the
   annotations.  The result, of course, might be completely insane --
   but it would have the rough justice of allowing you to describe
   code you don't understand with annotations you can't understand.

In Larch/C, I think, and in Larch/C++ the specification is not annotations
to the code.  It is in a separate file.

I do agree that macros are something that may be useful in the specification
language too.  Of course they could be abused, but so can universal
quantifiers.  Once one starts thinking about it, one can see the use
of macros in a specification language.  Also other ideas,
such as (higher-order!) functions on specifications might be useful.
At the moment we are limited by our ability (and time) to describe and explain
the use of such fancy constructs.

	Gary Leavens

	229 Atanasoff Hall, Department of Computer Science
	Iowa State University, Ames, Iowa 50011-1040 USA/leavens@cs.iastate.edu
	phone: (515) 294-1580 fax: (515) 294-0258 ftp site: ftp.cs.iastate.edu