[antlr-interest] Javadoc - static verification
Matthew Ford
Matthew.Ford at forward.com.au
Wed Oct 8 04:14:11 PDT 2003
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/
More information about the antlr-interest
mailing list