[antlr-interest] Javadoc - static verification

[Matthew Ford]

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/