Re: ADA Popularity Discussion Request

[jayessay <nospam@foo.com>]

Georg Bauhaus <sb463ba@l1-hrz.uni-duisburg.de> writes:

> jayessay <nospam@foo.com> wrote:
>  
> : If you wanted you could implement the whole Eiffel Dbc thing (and then
> : some) as a set of macros using CLOS within Common Lisp.  As I recall
> : now, someone actually did this (I will try to find it).
> 
> Whether you can implement static DbC in CLOS is the more intereisting
> question. Compare to SPARK.

Yes, that is exactly the idea.  You would create a set of macros to
allow a natural expression for this.  Macros do all their work at
compile time.  Macros are "just" functions which are code transformers
- you have the entire power of Lisp available and can write complete
compilers (lex -> syntax -> ast -> semantic analysis -> optimization
-> code generation) and have the result integrated transparently with
the rest of the language.

ACL2 is another example of this sort thing.  It is an applicative
system with type inference and theorem proving used by Motorola, AMD,
Rockwell Collins, et.al. for modeling and proving properties of
commercial microprocessors.


/Jon

-- 
'j' - a n t h o n y at romeo/charley/november com