Incorrect grammar for 'forall-var-declarator' in reference manual?

[Robert Dyer]

I have a question regarding the grammar for JML, as shown in the JML
reference manual.  Regarding 'forall variable declarations' in method
specifications, this is the listed grammar:

  forall-var-declarator ::= forall [ bound-var-modifiers ]
quantified-var-declarator ;

This seems wrong.  First, there is no mention of the type.  Something
like this would include the type:

  forall-var-declarator ::= forall [ bound-var-modifiers ] types-spec
quantified-var-declarator ;

But this also seems wrong based on some of the JDK specs I have seen,
which actually looks to have this grammar:

  forall-var-declarator ::= forall quantified-var-decls ;

This allows syntax of the form 'forall T x, y, z;' -- is this the
correct grammar?  Thanks.

--

Robert Dyer
rdyer@...

------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day
trial. Simplify your report design, integration and deployment - and focus on
what you do best, core application coding. Discover what's new with
Crystal Reports now.  http://p.sf.net/sfu/bobj-july
_______________________________________________
Jmlspecs-interest mailing list
Jmlspecs-interest@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest

[Gary T. Leavens-2]

Hi Rob, (and all),

Thanks for pointing this out, Rob, I believe you are correct that the
grammar in section 11.4.24 of the JML Reference Manual should be
something like (which it seems to be in version 1787 of the
JMLdocuments SVN; I'm not sure what version you are quoting :-).

spec-quantified-expr ::= ( quantifier quantified-var-decls ;
                            [ [ predicate ] ; ]
                            spec-expression )
quantifier ::= \forall | \exists
         | \max | \min
         | \num_of | \product | \sum
quantified-var-decls ::= [ bound-var-modifiers ] type-spec
                            quantified-var-declarator
                          [ , quantified-var-declarator ] ...
quantified-var-declarator ::= ident [ dims ]

I don't think there's a need for a separate production for \forall (as
opposed to the other kinds of spec-quantified-expr).

There is also a proposal in the wiki about some changes to
spec-quantified-exprs. See
   http://sourceforge.net/apps/trac/jmlspecs/wiki/QuantifierChanges for
details of that.

On Mon, 7 Sep 2009, Robert Dyer wrote:

> I have a question regarding the grammar for JML, as shown in the JML
> reference manual.  Regarding 'forall variable declarations' in method
> specifications, this is the listed grammar:
>
>  forall-var-declarator ::= forall [ bound-var-modifiers ]
> quantified-var-declarator ;
>
> This seems wrong.  First, there is no mention of the type.  Something
> like this would include the type:
>
>  forall-var-declarator ::= forall [ bound-var-modifiers ] types-spec
> quantified-var-declarator ;
>
> But this also seems wrong based on some of the JDK specs I have seen,
> which actually looks to have this grammar:
>
>  forall-var-declarator ::= forall quantified-var-decls ;
>
> This allows syntax of the form 'forall T x, y, z;' -- is this the
> correct grammar?  Thanks.

Yes, that seems right.

         Gary T. Leavens
         439C Harris Center (Bldg. 116)
         School of EECS, University of Central Florida
         4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
         http://www.eecs.ucf.edu/~leavens  phone: [phone]
         leavens@...

------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day
trial. Simplify your report design, integration and deployment - and focus on
what you do best, core application coding. Discover what's new with
Crystal Reports now.  http://p.sf.net/sfu/bobj-july
_______________________________________________
Jmlspecs-interest mailing list
Jmlspecs-interest@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest

[Robert Dyer]

Hi Gary,

I believe I was not quite clear when I posted earlier, so let me
clarify.  The grammar I was curious about is the forall variable
declarators which appear in 9.9.1.1 of the reference manual:

http://www.eecs.ucf.edu/~leavens/JML/jmlrefman/jmlrefman_9.html#SEC102

That is, the method specification clause and not the quantified
\forall expression.  I believe the quantified \forall expression is
correct in the manual I am viewing.

On Mon, Sep 7, 2009 at 8:38 PM, Gary T. Leavens<leavens@...> wrote:

> Hi Rob, (and all),
>
> Thanks for pointing this out, Rob, I believe you are correct that the
> grammar in section 11.4.24 of the JML Reference Manual should be
> something like (which it seems to be in version 1787 of the
> JMLdocuments SVN; I'm not sure what version you are quoting :-).
>
> spec-quantified-expr ::= ( quantifier quantified-var-decls ;
>                           [ [ predicate ] ; ]
>                           spec-expression )
> quantifier ::= \forall | \exists
>        | \max | \min
>        | \num_of | \product | \sum
> quantified-var-decls ::= [ bound-var-modifiers ] type-spec
>                           quantified-var-declarator
>                         [ , quantified-var-declarator ] ...
> quantified-var-declarator ::= ident [ dims ]
>
> I don't think there's a need for a separate production for \forall (as
> opposed to the other kinds of spec-quantified-expr).
>
> There is also a proposal in the wiki about some changes to
> spec-quantified-exprs. See
>  http://sourceforge.net/apps/trac/jmlspecs/wiki/QuantifierChanges for
> details of that.
>
> On Mon, 7 Sep 2009, Robert Dyer wrote:
>
>> I have a question regarding the grammar for JML, as shown in the JML
>> reference manual.  Regarding 'forall variable declarations' in method
>> specifications, this is the listed grammar:
>>
>>  forall-var-declarator ::= forall [ bound-var-modifiers ]
>> quantified-var-declarator ;
>>
>> This seems wrong.  First, there is no mention of the type.  Something
>> like this would include the type:
>>
>>  forall-var-declarator ::= forall [ bound-var-modifiers ] types-spec
>> quantified-var-declarator ;
>>
>> But this also seems wrong based on some of the JDK specs I have seen,
>> which actually looks to have this grammar:
>>
>>  forall-var-declarator ::= forall quantified-var-decls ;
>>
>> This allows syntax of the form 'forall T x, y, z;' -- is this the
>> correct grammar?  Thanks.
>
> Yes, that seems right.
>
>        Gary T. Leavens
>        439C Harris Center (Bldg. 116)
>        School of EECS, University of Central Florida
>        4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
>        http://www.eecs.ucf.edu/~leavens  phone: [phone]
>        leavens@...
>

--

Robert Dyer
rdyer@...

------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day
trial. Simplify your report design, integration and deployment - and focus on
what you do best, core application coding. Discover what's new with
Crystal Reports now.  http://p.sf.net/sfu/bobj-july
_______________________________________________
Jmlspecs-interest mailing list
Jmlspecs-interest@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest