\invariant_for executability in the new semantics

View: New views

2 Messages — Rating Filter: Alert me

\invariant_for executability in the new semantics

by Wladimir de Lara Araujo Filho :: Rate this Message:

Reply to Author | View Threaded | Show Only this Message

Some parts of this message have been removed. Learn more about Nabble's security policy.

Hi,

I am updating the JML2 RAC to support inner classes (amongst other things) and I encountered a situation with the racrun/InvariantFor3.java testcase. When run in the new semantics (jmlc -T), jmlc complains that invariant_for expression is not executable. This does not affect in any way my changes but I’d like to ask if there is a reason for its “non-executability”. My changes are still based on JML 5.4, so this might have been updated later on. If that’s the case, please let me know so I can merge this into my private branch.

Cheers,

Wladimir de Lara Araujo Filho
260 Besserer St. suite 602
Ottawa-ON Canada
K1N 1J3
Phone (613) 232-3990

There are three schools of magic.
One: State a tautology, then ring the changes on its
corollaries; that's philosophy.
Two: Record many facts. Try to find a pattern.
Then make a wrong guess at the next fact; that's science.
Three: Be aware that you live in a malevolent Universe controlled
by Murphy's Law, sometimes offset by
Brewster's Factor; that's engineering.
-- Robert A. Heinlein

-------------------------------------------------------------------------
Check out the new SourceForge.net Marketplace.
It's the best place to buy or sell services for
just about anything Open Source.
http://sourceforge.net/services/buy/index.php
_______________________________________________
Jmlspecs-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers

Re: \invariant_for executability in the new semantics

by Gary T. Leavens-2 :: Rate this Message:

Reply to Author | View Threaded | Show Only this Message

Hi Wladimir,

On Sun, 29 Jun 2008, Wladimir de Lara Araujo Filho wrote:

> I am updating the JML2 RAC to support inner classes (amongst
> other things) and I encountered a situation with the
> racrun/InvariantFor3.java testcase. When run in the new semantics (jmlc -T),
> jmlc complains that invariant_for expression is not executable. This does
> not affect in any way my changes but I'd like to ask if there is a reason
> for its "non-executability". My changes are still based on JML 5.4, so this
> might have been updated later on. If that's the case, please let me know so
> I can merge this into my private branch.

There is no special reason why the \invariant_for expression should
not be executable. Indeed, we'd like it to be executable. Also if
you have enhanced support for inner classes, that would also be great.
If you have the time to merge these fixes and improvements into the
main branch of JML2, please do so. Thanks,

Gary T. Leavens
210 Harris Center (Bldg. 116)
School of EECS, University of Central Florida
4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
http://www.eecs.ucf.edu/~leavens phone: +1-407-823-4758
leavens@...

-------------------------------------------------------------------------
Sponsored by: SourceForge.net Community Choice Awards: VOTE NOW!
Studies have shown that voting for your favorite open source project,
along with a healthy diet, reduces your potential for chronic lameness
and boredom. Vote Now at http://www.sourceforge.net/community/cca08
_______________________________________________
Jmlspecs-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers

LightInTheBox - Buy quality products at wholesale price!