Re: [Grammatica-users] JML Parser

[Per Cederberg]

On Mon, 2004-03-22 at 05:06, Brandon Silverstein wrote:
> Hello,
> 
> I am new to Grammatica and I am trying to develop a JML parser in C#.  
> I am converting the grammar found at 
> http://www.cs.iastate.edu/~leavens/JML/jmlrefman/jmlrefman_20.html to a 
> format that Grammatica can understand and parse.  After creating a 
> whole bunch of tokens and reformatting the file, I am getting 
> individual errors saying:
> 
> production 'myProduction' is invalid, as zero elements can be matched 
> (minimum is one)

What Grammatica is trying to say is that this is an invalid 
production:

A = "hello"
  | ;          <- this alternative is empty (zero elements)

Instead, you should use the following:

A = "hello" ;

And each time you refer to A, use "[A]" or "A?" instead of plain 
"A", like this:

B = A? "world" ;

> I've tried to figure out what the problem is, and I think it has 
> something to do with reformatting the "optional" text in the original 
> JML file.  Anytime a ... appears, I surround the optional text with { 
> brackets }.  Anyway, I made a test file with the example production 
> shown in the Grammatica reference manual.
> 
> Prod = "1"? | "2"* ...... and so on.  When I try to parse this file, I 
> get the same error message.

Ok, the example wasn't so well chosen maybe. As you found out the
hard way, figure 2 contains an invalid production that was just 
supposed to illustrate the various quantifies that exist. The 
example is invalid for the same reason as above:

Prod = "1"?          <- invalid, can match empty input
     | "2"*          <- invalid, can match empty input
     | "3"+
     | {"4"}         <- invalid, can match empty input
     | ["5"] ;       <- invalid, can match empty input

This limitation exists in Grammatica due to the token look-ahead
calculation. Basically, if Grammatica allows productions that 
can match empty input, we may get into tricky situations:

A = B* C ;
B = ;

Now, one might argue that it is the A rule that is invalid in
this case (as you never know when to go on to C), but the 
implementation was much simplified if Grammatica can assume that
all productions matches at least one token.

> I am intrigued by the statement right 
> below the yellow box where this production is located in the manual.  
> It states that Grammatica does not allow null production alternatives, 
> but "the same result can be obtained by making all references to the 
> production optional."  I still can't figure out how to solve this 
> problem.

Some versions of EBNF does not just leave the production empty,
but instead writes the previous example like this:

A = B* C ;
B = null ;

Using "null" instead of empty to avoid confusion.

> Any help is appreciated.

A small example of how a part of your JML grammar would look in
Grammatica:

/* Not needed, refer to Modifier* instead */
Modifiers = Modifier+ ;
Modifier = "public"
         | "private"
         | "protected"
         | "spec_public"
         | "spec_protected"
         | "abstract"
         | "static"
         | "model"
         | "ghost"
         | "pure"
         | "final"
         | "synchronized"
         | "instance"
         | "helper"
         | "transient"
         | "volatile"
         | "native"
         | "strictfp"
         | "const"
         | "non_null" ;

Then you'd use it like this:

Field = DOC_COMMENT* Modifier* MemberDecl
      | Modifier* JmlDeclaration
      | [MethodSpecification] ["static"] CompoundStatement
      | MethodSpecification StaticInitializer
      | MethodSpecification Initializer
      | "axiom" Predicate ;

BTW, you'll have to rewrite the above Field declaration. I'm
only showing it here to make it clear how to refer to the
"Modifier" production.

The problem in Java (and C++) is that for a field declaration,
the number of look-ahead tokens before being able to 
distinguish between the alternatives is possibly infinite. So
Grammatica cannot calculate look-ahead sets for the above 
alternatives. Instead, you'll probably end up with something
more like this (untested, just an example):

Field = FieldDeclaration
      | FieldStatement
      | FieldInitializerOrStatement
      | FieldAxiom ;

FieldDeclaration = DOC_COMMENT* Modifier* Declaration ;

FieldStatement = ["static"] CompoundStatement ;

FieldInitializerOrStatement = 
    MethodSpecification InitializerOrStatement ;

FieldAxiom = "axiom" Predicate ;

Declaration = MemberDecl
            | JmlDecl ;

InitializerOrStatement = FieldStatement
                       | StaticInitializer
                       | Initializer ;

Hope this helps!

Cheers,

/Per