Re: Verified compilers?

["Randy Brukardt" <randy@rrsoftware.com>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1psd0g0womgxi.1sle7ol12x3d5.dlg@40tude.net...
...
> Furthermore the merits of formal grammar definitions are debatable, 
> because
> the complexity of grammar descriptions usually make it impossible to judge
> if a given string do belong to the formal language or not. Normally BNF is
> all one needs to define syntax.

This makes no sense at all. BNF is the classic formal definition of a 
grammar; indeed, I know of no other. Everybody has variations on it (the Ada 
BNF uses repeat operations not found in many BNFs; the annoted BNF used by 
our grammar generator is slightly different), but they're all forms of BNF.

Perhaps you are talking about grammar generator processessable 
definitions -- that's a different beast altogether and forms just a tiny 
portion of "formal grammar definitions".

As far as LR parsing is concerned, that's the most general practical parsing 
scheme. There are many legitmate BNFs that cannot be parsed using recursive 
descent. And writing recursive descent code (and error handling) is many 
times harder than adding a couple of lines to a file and lanuching a batch 
file:

          Aspect_Specification ::= WITH Aspect_Item {, Aspect_Item}
          Aspect_Item ::= IDENTIFIER => Expression

[although I admit this is a small portion of the total work; it took me 
about 4 weeks to add the entire Ada 2005 syntax to Janus/Ada, but probably 
only about an hour or two on the actual grammar. The rest of the time was 
spent adding "unimplemented feature" error handlers to the compiler, 
adjusting existing parts of the compiler to be aware of the changes (new 
grammar features changing the stack position of old ones), updating the 
pretty printer to be aware of the new features, and the like.]

                                    Randy.