[antlr-interest] Javadoc - static verification

[guyveraghtert]

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/