[antlr-interest] Javadoc - static verification

Matthew Ford Matthew.Ford at forward.com.au
Wed Oct 8 14:30:34 PDT 2003


Actually this was only a partial answer.

If I understand you correctly there are actually two types of  ID
WORD at pre and WORD at post

In the @pre section  the ID WORD is actually a shorthand for WORD at pre
In the @post section  the ID WORD is actually a shorthand for WORD at post

So I think you need to add a rule to your lexer to find
WORD at pre and WORD at post
I needs to be in the lexer to overcome the whitespace problem
(I assume  "WORD @pre"  is not valid due to the whitespace.)

The rules would be something like

// word at pre
WORD_PRE
// words can't contain whitespace, an '@'-symbol, '*'-symbol or
'|'-symbol
: WORD @ ('p'|'P')('r'|'R')('e'|'E')
;

// word at post
WORD_POST
// words can't contain whitespace, an '@'-symbol, '*'-symbol or
'|'-symbol
: WORD @ ('p'|'P')('o'|'O')('s'|'S')('t'|'T')
;

I haven't actually tried these rules, but you get the idea.

matthew

----- Original Message ----- 
From: "Matthew Ford" <Matthew.Ford at forward.com.au>
To: <antlr-interest at yahoogroups.com>
Sent: Wednesday, October 08, 2003 9:14 PM
Subject: Re: [antlr-interest] Javadoc - static verification


> It looks to me like
> you could use the |  in @post tag statement to start looking for @pre
>
>  | flip != flip at pre
>
> @pre elsewhere should be a tag?
>
> matthew
> ----- Original Message ----- 
> From: "guyveraghtert" <guyveraghtert at yahoo.com>
> To: <antlr-interest at yahoogroups.com>
> Sent: Wednesday, October 08, 2003 6:07 PM
> Subject: [antlr-interest] Javadoc - static verification
>
>
> > Hi all
> >
> > I'm working on a project to statically check your code against your
> > specification. We use Jnome (www.jnome.org), which offers a metamodel
> > for java. However, this metamodel represents the formal specification
> > as a string. This should be adapted: the formal specifications are
> > just java expressions. Only one problem exists, one can use the OCL
> > notation @pre te refer to the 'state' of an expression before entering
> > a method. I give an example:
> >
> > /**
> >  * Class representing a flipflop
> >  */
> > public class FlipFlop{
> >
> >   /**
> >    * Variable expressing state of flipflop
> >    */
> >   private boolean flip;
> >
> >   /**
> >    * Flip the flipflop
> >    *
> >    * @post     The flipflop flipped
> >    *         | flip != flip at pre
> >    */
> >   public void flipflop(){
> >     flip != flip;
> >   }
> >
> > }
> >
> >
> > Another problem is the fact we do not only have the OCL notation
> > '@pre', but also a tag '@pre':
> >
> > ...
> >
> >  /**
> >   * Set the name
> >   *
> >   * @pre    <name> must be effective
> >   *       | name != null
> >   * @post   <name> is set as the name of this entity
> >   *       | getName() == name
> >   */
> >  public void setName(String name){
> >      this.name = name;
> >  }
> >
> > ...
> >
> > The current grammar of jnome for javadoc is:
> >
> >
> >
>
//--------------------------------------------------------------------------
> --
> > // The parser
> >
>
//--------------------------------------------------------------------------
> --
> >
> > header {
> > package org.jnome.input.antlr.javadoc.parser;
> > }
> >
> > class JavaDocParser extends Parser;
> > options {
> > exportVocab=JavaDoc;             // Call its vocabulary "JavaDoc"
> > buildAST = true;                 // build an AST
> > }
> >
> > tokens {
> > JAVADOC_OPEN; JAVADOC_CLOSE; STAR; TAG; WORD; DESCRBLOCK; VERTICAL_LINE;
> > FORMAL; INFORMAL; NEWLINE; AT; TAGBLOCK; SENTENCEFORMAL;
> > }
> >
> > // a specification block
> > specificationBlock
> > :   // A block to describe the method/class/variable/.. briefly
> > (descriptionBlock)?
> >
> > // A series of blocks starting with an @-tag
> > (tagBlock)*
> >
> > // The end of the specification ("*/")
> > JAVADOC_CLOSE!
> > ;
> >
> > // the short description at the beginning of a specification block
> > descriptionBlock
> > : (sentence)+
> > {#descriptionBlock = #([DESCRBLOCK, "DESCRBLOCK"], #descriptionBlock);}
> > ;
> >
> > // a part of a specification block, starting with an @-tag
> > tagBlock
> > : tag
> > (informalSpecification)
> > (formalSpecification (emptySentence)* )?
> > {#tagBlock = #([TAGBLOCK, "TAGBLOCK"], #tagBlock);}
> > ;
> >
> > // an '@'-tag
> > tag
> > : AT! WORD
> >   {#tag = #([TAG, "TAG"], #tag);}
> > ;
> >
> > // the informal specification in a tagblock
> > informalSpecification
> > : (sentence)+
> > {#informalSpecification = #([INFORMAL, "INFORMAL"],
> > #informalSpecification);}
> > ;
> >
> > // the formal specification in a tagblock
> > formalSpecification
> > : (sentenceFormal)+
> > {#formalSpecification = #([FORMAL, "FORMAL"], #formalSpecification);}
> > ;
> >
> > // a sentence can be empty or not
> > sentence
> > :   emptySentence | nonEmptySentence
> > ;
> >
> > // a non empty sentence
> > nonEmptySentence
> > :   WORD (WORD|STAR|AT|VERTICAL_LINE)* endline
> > ;
> >
> > // an empty sentence
> > emptySentence
> > :   endline
> > ;
> >
> > // a sentence from a formal specification
> > sentenceFormal
> > :   VERTICAL_LINE! (WORD|STAR|AT|VERTICAL_LINE)* endline
> > {#sentenceFormal = #([SENTENCEFORMAL, "SENTENCEFORMAL"],
> > #sentenceFormal);}
> > ;
> >
> > // a newline symbol, followed by zero or more stars
> > endline!
> > :   ( NEWLINE(STAR)* )
> > ;
> >
> >
>
//--------------------------------------------------------------------------
> --
> > // The lexer
> >
>
//--------------------------------------------------------------------------
> --
> >
> > // Import the necessary classes
> > {
> > import antlr.TokenStreamSelector;
> > }
> >
> > class JavaDocLexer extends Lexer;
> >
> > options {
> > exportVocab=JavaDoc;   // call the vocabulary "JavaDoc"
> > testLiterals=true;     // automatically test for literals
> > k=2;                   // two characters of lookahead
> > }
> >
> > // let the lexer know about the selector
> > {
> > protected TokenStreamSelector selector;
> >
> > public JavaDocLexer(LexerSharedInputState state, TokenStreamSelector
> > sel) {
> > this(state);
> > selector = sel;
> > }
> >
> > }
> >
> > // a dummy rule to force vocabulary to be all characters (except special
> > //   ones that ANTLR uses internally (0 to 2)
> > protected
> > VOCAB
> > : '\3'..'\377'
> > ;
> >
> > // end of specification block
> > JAVADOC_CLOSE
> > : "*/"
> > { selector.pop(); }
> > ;
> >
> > // @-symbol
> > AT
> > : '@'
> > ;
> >
> > // star
> > STAR
> > : '*'
> > ;
> >
> > // vertical line
> > VERTICAL_LINE
> > : '|'
> > ;
> >
> > // word
> > WORD
> > // words can't contain whitespace, an '@'-symbol, '*'-symbol or
> > '|'-symbol
> > : (~( ' ' | '\t' | '\f' | '\r' | '\n' | '@' | '*' | '|'))+
> > ;
> >
> > // Whitespace -- ignored
> > WS : ( ' '
> > | '\t'
> > | '\f'
> > )
> > { _ttype = Token.SKIP; }
> > ;
> >
> > // newline character
> > NEWLINE
> > : // handle newlines
> > ( "\r\n"  // Evil DOS
> > | '\r'    // Macintosh
> > | '\n'    // Unix
> > )
> > { newline(); }
> > ;
> >
> > -----------------------------------------------------------------
> >
> > How can we easily adapt this grammar to our needs?
> >
> > A minor problem, this grammar doesn't support
> > single line comments /*  */ . The authors told me they didn't how to
> > fix is (ambiguities).
> >
> > I ask a lot, but any help is welcome...
> >
> > thx
> >
> > Guy
> >
> >
> >
> >
> >
> >
> > Your use of Yahoo! Groups is subject to
http://docs.yahoo.com/info/terms/
> >
> >
>
>
>
>
> Your use of Yahoo! Groups is subject to http://docs.yahoo.com/info/terms/
>
>


 

Your use of Yahoo! Groups is subject to http://docs.yahoo.com/info/terms/ 




More information about the antlr-interest mailing list