Eclipse Community Forums: Epsilon » Preconditions and postconditions for operations and ErlParserRules.g

Help

Home

Home » Modeling » Epsilon » Preconditions and postconditions for operations and ErlParserRules.g

Show: Today's Messages :: Show Polls :: Message Navigator

Preconditions and postconditions for operations and ErlParserRules.g [message #479404]

Mon, 10 August 2009 21:27

Eclipse User

Originally posted by: nyoescape.gmail.com

Hello everyone,

I tried adding a precondition executable annotation to an operation
which I'd use as part of an EVL module, and ran into some problems.

For instance, the canonical example from the Epsilon book shows several
parsing errors:

$pre i > 0 <-- **here**
$post _result > self <- **and here**
operation Integer add(i : Integer) : Integer {
return self + i;
}

I've been poking around the grammar files and EVL files can contain
annotationBlock symbols, which are formed by one or more annotations,
which can be either Annotations (@likethis) or executableAnnotations
(the $pre and $post lines in the previous example, if I'm not mistaken).

However, Evl.g also imports the ErlParserRules.g, which define the pre
and post named blocks like this:

pre
: p='pre'^ NAME? statementBlock
{$p.setType(PRE);}
;

post
: p='post'^ NAME? statementBlock
{$p.setType(POST);}
;

I don't know much about ANTLR (I have only used JavaCC and flex/bison),
but from what I've been able to debug, it seems that the lexer processes
the 'pre' as the ERL 'pre': it goes to EvlLexer#mT__131, which contains
a 'match("pre");' line, instead of Evl_EolLexerRules#mNAME.

However, the scanner does use the executableAnnotation rule, but since
there's the wrong token in the stream, it reports a parse error.

If I change it to this, it works, but obviously they're not interpreted
as preconditions and postconditions anymore:

$Pre i > 0
$Post _result > self
operation Integer add(i : Integer) : Integer {
return self + i;
}

This also parses correctly:

pre { i > 0; }
post { _result > self; }
operation Integer add(i : Integer) : Integer {
return self + i;
}

I'm not sure how to deal with this problem. Perhaps we could change the
name for the precondition and postcondition executable annotations to
$requires and $ensures, as in JML, or simply $Pre and $Post? However,
the "$pre ..." syntax would still fail, though it's valid, according to
the documentation. :-/

Regards,
Antonio

Report message to a moderator

Re: Preconditions and postconditions for operations and ErlParserRules.g [message #479469 is a reply to message #479404]

Tue, 11 August 2009 09:09

Louis Rose

Messages: 440
Registered: July 2009
Location: York, United Kingdom

Senior Member

Hi Antonio,

Thanks for the thorough investigation. I can see how the pre annotation
might cause problems in languages that inherit from ERL.

I'll see if I can recreate this problem later today. We may be able to
use some ANTLR cleverness to handle this case.

Cheers,
Louis.

Antonio García Domínguez wrote:
> Hello everyone,
>
> I tried adding a precondition executable annotation to an operation
> which I'd use as part of an EVL module, and ran into some problems.
>
> For instance, the canonical example from the Epsilon book shows several
> parsing errors:
>
> $pre i > 0 <-- **here**
> $post _result > self <- **and here**
> operation Integer add(i : Integer) : Integer {
> return self + i;
> }
>
> I've been poking around the grammar files and EVL files can contain
> annotationBlock symbols, which are formed by one or more annotations,
> which can be either Annotations (@likethis) or executableAnnotations
> (the $pre and $post lines in the previous example, if I'm not mistaken).
>
> However, Evl.g also imports the ErlParserRules.g, which define the pre
> and post named blocks like this:
>
> pre
> : p='pre'^ NAME? statementBlock
> {$p.setType(PRE);}
> ;
>
> post
> : p='post'^ NAME? statementBlock
> {$p.setType(POST);}
> ;
>
> I don't know much about ANTLR (I have only used JavaCC and flex/bison),
> but from what I've been able to debug, it seems that the lexer processes
> the 'pre' as the ERL 'pre': it goes to EvlLexer#mT__131, which contains
> a 'match("pre");' line, instead of Evl_EolLexerRules#mNAME.
>
> However, the scanner does use the executableAnnotation rule, but since
> there's the wrong token in the stream, it reports a parse error.
>
> If I change it to this, it works, but obviously they're not interpreted
> as preconditions and postconditions anymore:
>
> $Pre i > 0
> $Post _result > self
> operation Integer add(i : Integer) : Integer {
> return self + i;
> }
>
> This also parses correctly:
>
> pre { i > 0; }
> post { _result > self; }
> operation Integer add(i : Integer) : Integer {
> return self + i;
> }
>
> I'm not sure how to deal with this problem. Perhaps we could change the
> name for the precondition and postcondition executable annotations to
> $requires and $ensures, as in JML, or simply $Pre and $Post? However,
> the "$pre ..." syntax would still fail, though it's valid, according to
> the documentation. :-/
>
> Regards,
> Antonio

Report message to a moderator

Re: Preconditions and postconditions for operations and ErlParserRules.g [message #479594 is a reply to message #479404]

Tue, 11 August 2009 16:32

Louis Rose

Messages: 440
Registered: July 2009
Location: York, United Kingdom

Senior Member

Hi Antonio,

I'm just starting to look at this. I've been able to recreate the problem.

For now, a workaround is to define your annotated operation in an EOL file:

$pre i > 0 <-- **here**
$post _result > self <- **and here**
operation Integer add(i : Integer) : Integer {
return self + i;
}

And then import it into your EVL file:

import 'add.evl';

context MyModelElement {

constraint MyConstraint {
check: self.size() = 2.add(-1); -- fails with unsatisifed
precondition exception
}

}

I'll see if I can fix the parser so this doesn't happen. Could you open
a bug report? Thanks!

Cheers,
Louis.

Antonio García Domínguez wrote:
> Hello everyone,
>
> I tried adding a precondition executable annotation to an operation
> which I'd use as part of an EVL module, and ran into some problems.
>
> For instance, the canonical example from the Epsilon book shows several
> parsing errors:
>
> $pre i > 0 <-- **here**
> $post _result > self <- **and here**
> operation Integer add(i : Integer) : Integer {
> return self + i;
> }
>
> I've been poking around the grammar files and EVL files can contain
> annotationBlock symbols, which are formed by one or more annotations,
> which can be either Annotations (@likethis) or executableAnnotations
> (the $pre and $post lines in the previous example, if I'm not mistaken).
>
> However, Evl.g also imports the ErlParserRules.g, which define the pre
> and post named blocks like this:
>
> pre
> : p='pre'^ NAME? statementBlock
> {$p.setType(PRE);}
> ;
>
> post
> : p='post'^ NAME? statementBlock
> {$p.setType(POST);}
> ;
>
> I don't know much about ANTLR (I have only used JavaCC and flex/bison),
> but from what I've been able to debug, it seems that the lexer processes
> the 'pre' as the ERL 'pre': it goes to EvlLexer#mT__131, which contains
> a 'match("pre");' line, instead of Evl_EolLexerRules#mNAME.
>
> However, the scanner does use the executableAnnotation rule, but since
> there's the wrong token in the stream, it reports a parse error.
>
> If I change it to this, it works, but obviously they're not interpreted
> as preconditions and postconditions anymore:
>
> $Pre i > 0
> $Post _result > self
> operation Integer add(i : Integer) : Integer {
> return self + i;
> }
>
> This also parses correctly:
>
> pre { i > 0; }
> post { _result > self; }
> operation Integer add(i : Integer) : Integer {
> return self + i;
> }
>
> I'm not sure how to deal with this problem. Perhaps we could change the
> name for the precondition and postcondition executable annotations to
> $requires and $ensures, as in JML, or simply $Pre and $Post? However,
> the "$pre ..." syntax would still fail, though it's valid, according to
> the documentation. :-/
>
> Regards,
> Antonio

Report message to a moderator

Re: Preconditions and postconditions for operations and ErlParserRules.g [message #479604 is a reply to message #479594]

Tue, 11 August 2009 16:57

Louis Rose

Messages: 440
Registered: July 2009
Location: York, United Kingdom

Senior Member

I can't think of a straightforward solution to this right now. I think
I'll need to speak with Dimitrios when he returns from vacation. Let me
know if the workaround causes any further problems for you, and I'll
have another attempt at fixing this.

Cheers,
Louis.

Louis Rose wrote:
> Hi Antonio,
>
> I'm just starting to look at this. I've been able to recreate the problem.
>
> For now, a workaround is to define your annotated operation in an EOL file:
>
> $pre i > 0 <-- **here**
> $post _result > self <- **and here**
> operation Integer add(i : Integer) : Integer {
> return self + i;
> }
>
> And then import it into your EVL file:
>
> import 'add.evl';
>
> context MyModelElement {
>
> constraint MyConstraint {
> check: self.size() = 2.add(-1); -- fails with unsatisifed
> precondition exception
> }
>
> }
>
> I'll see if I can fix the parser so this doesn't happen. Could you open
> a bug report? Thanks!
>
> Cheers,
> Louis.
>
> Antonio García Domínguez wrote:
>> Hello everyone,
>>
>> I tried adding a precondition executable annotation to an operation
>> which I'd use as part of an EVL module, and ran into some problems.
>>
>> For instance, the canonical example from the Epsilon book shows several
>> parsing errors:
>>
>> $pre i > 0 <-- **here**
>> $post _result > self <- **and here**
>> operation Integer add(i : Integer) : Integer {
>> return self + i;
>> }
>>
>> I've been poking around the grammar files and EVL files can contain
>> annotationBlock symbols, which are formed by one or more annotations,
>> which can be either Annotations (@likethis) or executableAnnotations
>> (the $pre and $post lines in the previous example, if I'm not mistaken).
>>
>> However, Evl.g also imports the ErlParserRules.g, which define the pre
>> and post named blocks like this:
>>
>> pre
>> : p='pre'^ NAME? statementBlock
>> {$p.setType(PRE);}
>> ;
>>
>> post
>> : p='post'^ NAME? statementBlock
>> {$p.setType(POST);}
>> ;
>>
>> I don't know much about ANTLR (I have only used JavaCC and flex/bison),
>> but from what I've been able to debug, it seems that the lexer processes
>> the 'pre' as the ERL 'pre': it goes to EvlLexer#mT__131, which contains
>> a 'match("pre");' line, instead of Evl_EolLexerRules#mNAME.
>>
>> However, the scanner does use the executableAnnotation rule, but since
>> there's the wrong token in the stream, it reports a parse error.
>>
>> If I change it to this, it works, but obviously they're not interpreted
>> as preconditions and postconditions anymore:
>>
>> $Pre i > 0
>> $Post _result > self
>> operation Integer add(i : Integer) : Integer {
>> return self + i;
>> }
>>
>> This also parses correctly:
>>
>> pre { i > 0; }
>> post { _result > self; }
>> operation Integer add(i : Integer) : Integer {
>> return self + i;
>> }
>>
>> I'm not sure how to deal with this problem. Perhaps we could change the
>> name for the precondition and postcondition executable annotations to
>> $requires and $ensures, as in JML, or simply $Pre and $Post? However,
>> the "$pre ..." syntax would still fail, though it's valid, according to
>> the documentation. :-/
>>
>> Regards,
>> Antonio

Report message to a moderator

Re: Preconditions and postconditions for operations and ErlParserRules.g [message #479762 is a reply to message #479404]

Wed, 12 August 2009 12:55

Louis Rose

Messages: 440
Registered: July 2009
Location: York, United Kingdom

Senior Member

Bug 286385 covers this issue:

https://bugs.eclipse.org/bugs/show_bug.cgi?id=286385

Antonio García Domínguez wrote:
> Hello everyone,
>
> I tried adding a precondition executable annotation to an operation
> which I'd use as part of an EVL module, and ran into some problems.
>
> For instance, the canonical example from the Epsilon book shows several
> parsing errors:
>
> $pre i > 0 <-- **here**
> $post _result > self <- **and here**
> operation Integer add(i : Integer) : Integer {
> return self + i;
> }
>
> I've been poking around the grammar files and EVL files can contain
> annotationBlock symbols, which are formed by one or more annotations,
> which can be either Annotations (@likethis) or executableAnnotations
> (the $pre and $post lines in the previous example, if I'm not mistaken).
>
> However, Evl.g also imports the ErlParserRules.g, which define the pre
> and post named blocks like this:
>
> pre
> : p='pre'^ NAME? statementBlock
> {$p.setType(PRE);}
> ;
>
> post
> : p='post'^ NAME? statementBlock
> {$p.setType(POST);}
> ;
>
> I don't know much about ANTLR (I have only used JavaCC and flex/bison),
> but from what I've been able to debug, it seems that the lexer processes
> the 'pre' as the ERL 'pre': it goes to EvlLexer#mT__131, which contains
> a 'match("pre");' line, instead of Evl_EolLexerRules#mNAME.
>
> However, the scanner does use the executableAnnotation rule, but since
> there's the wrong token in the stream, it reports a parse error.
>
> If I change it to this, it works, but obviously they're not interpreted
> as preconditions and postconditions anymore:
>
> $Pre i > 0
> $Post _result > self
> operation Integer add(i : Integer) : Integer {
> return self + i;
> }
>
> This also parses correctly:
>
> pre { i > 0; }
> post { _result > self; }
> operation Integer add(i : Integer) : Integer {
> return self + i;
> }
>
> I'm not sure how to deal with this problem. Perhaps we could change the
> name for the precondition and postcondition executable annotations to
> $requires and $ensures, as in JML, or simply $Pre and $Post? However,
> the "$pre ..." syntax would still fail, though it's valid, according to
> the documentation. :-/
>
> Regards,
> Antonio

Report message to a moderator