[antlr-interest] LL(*) proof

[Terence Parr]

On Oct 14, 2006, at 1:09 AM, Ilia Kantor wrote:

> В сообщении от 14 октября 2006 00:56 Terence  
> Parr написал(a):
>> On Oct 13, 2006, at 1:35 PM, Ilia Kantor wrote:
>>> I wrote a grammar for antlr v3. But I need to proff that it's
>>> 1) LL(*)
>>
>> ANTLR will tell you if it's LL(*).
>
> Could be nice to have a mathematical proof.. W
> hat's a definition of LL(*) ? How to prove that grammar is LL(*)  
> having its
> antlr notation ?

Yes, I hope to write a nice paper convincing you the algorithm is  
sound, but it will have to wait probably a year. :(

>>> 2) single program tree
>>
>> I'm not sure what you mean here.
>
> I have a grammar of (kindof) programming language.
> I guess, to make sure its correct, need to prove, that it  
> transforms a program
> into single, determined AST.

Well, it will always give you exactly one AST, but it would be hard  
to prove you get the one your brain intended.

Ter