ESCTools in Eclipse

[George Karabotsos-2]

Hello all,

I am wondering if anyone is working with the ESCTools code in Eclipse? 

I realized that it is possible to import the code but I get over 5K errors.  Has anyone run into the same kind of problems?  Is there a quick fix?

TIA,

George



-------------------------------------------------------------------------
This SF.net email is sponsored by DB2 Express
Download DB2 Express C - the FREE version of DB2 express and take
control of your XML. No limits. Just data. Click to get it now.
http://sourceforge.net/powerbar/db2/
_______________________________________________
JMLspecs-ESCJava mailing list
JMLspecs-ESCJava@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-escjava

[Joseph Kiniry]

Hi George,

On 8 Jun, 2007, at 3:03, George Karabotsos wrote:

> Hello all,
>
> I am wondering if anyone is working with the ESCTools code in Eclipse?

Yup, we all are here at UCD.  And other Mobius partners are starting  
to do all their development now within Eclipse (many already have  
been for several months).

> I realized that it is possible to import the code but I get over 5K  
> errors.  Has anyone run into the same kind of problems?  Is there a  
> quick fix?

We can give you a pre-configured workspace or project if you like.  
It is part of the upcoming public Mobius Program Verification  
Environment (beta) developer release.

We just distributed pre-release snapshots of all plugins and a  
developer workspace to Mobius partners this week at the Mobius 2nd  
annual meeting here in Dublin.

I'll put up the plugins snapshot and workspace snapshot on a private  
webserver and point you to it.  Sounds good?

Note that we have only tested it all on OS X and Linux at this  
moment.  If you are a Windows user you'll be our first Windows test  
subject. :)  We expect it all to "just work", as it did when we moved  
it to Linux this week for the first time.

Additionally, the new 2.0b1 release of ESC/Java2 runs in a Java 1.5+  
VM.  And, while it can process 1.5 bytecode, but do not parse 1.5  
source.

Joe

-------------------------------------------------------------------------
This SF.net email is sponsored by DB2 Express
Download DB2 Express C - the FREE version of DB2 express and take
control of your XML. No limits. Just data. Click to get it now.
http://sourceforge.net/powerbar/db2/
_______________________________________________
JMLspecs-ESCJava mailing list
JMLspecs-ESCJava@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-escjava

[Dermot Cochran]

On Jun 8, 2007, at 3:03 AM, George Karabotsos wrote:

> Hello all,
>
> I am wondering if anyone is working with the ESCTools code in Eclipse?

Yes, although it needs to be built from the command line using 'make'.

>
> I realized that it is possible to import the code but I get over 5K  
> errors.  Has anyone run into the same kind of problems?  Is there a  
> quick fix?
>
> TIA,
>
> George
>
>
> ----------------------------------------------------------------------
> ---
> This SF.net email is sponsored by DB2 Express
> Download DB2 Express C - the FREE version of DB2 express and take
> control of your XML. No limits. Just data. Click to get it now.
> http://sourceforge.net/powerbar/db2/
> _______________________________________________
> JMLspecs-ESCJava mailing list
> JMLspecs-ESCJava@...
> https://lists.sourceforge.net/lists/listinfo/jmlspecs-escjava

-------------------------------------------------------------------------
This SF.net email is sponsored by DB2 Express
Download DB2 Express C - the FREE version of DB2 express and take
control of your XML. No limits. Just data. Click to get it now.
http://sourceforge.net/powerbar/db2/
_______________________________________________
JMLspecs-ESCJava mailing list
JMLspecs-ESCJava@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-escjava

[Dermot Cochran]

On Jun 8, 2007, at 9:34 AM, Joseph Kiniry wrote:

> Hi George,
>
> On 8 Jun, 2007, at 3:03, George Karabotsos wrote:
>
>> Hello all,
>>
>> I am wondering if anyone is working with the ESCTools code in  
>> Eclipse?
>
> Yup, we all are here at UCD.  And other Mobius partners are starting
> to do all their development now within Eclipse (many already have
> been for several months).
>
>> I realized that it is possible to import the code but I get over 5K
>> errors.  Has anyone run into the same kind of problems?  Is there a
>> quick fix?

The 'quick fix' is to build from the command line using 'make'.

>
> We can give you a pre-configured workspace or project if you like.
> It is part of the upcoming public Mobius Program Verification
> Environment (beta) developer release.
>
> We just distributed pre-release snapshots of all plugins and a
> developer workspace to Mobius partners this week at the Mobius 2nd
> annual meeting here in Dublin.
>
> I'll put up the plugins snapshot and workspace snapshot on a private
> webserver and point you to it.  Sounds good?
>
> Note that we have only tested it all on OS X and Linux at this
> moment.  If you are a Windows user you'll be our first Windows test
> subject. :)  We expect it all to "just work", as it did when we moved
> it to Linux this week for the first time.
>
> Additionally, the new 2.0b1 release of ESC/Java2 runs in a Java 1.5+
> VM.  And, while it can process 1.5 bytecode, but do not parse 1.5
> source.
>
> Joe
>
> ----------------------------------------------------------------------
> ---
> This SF.net email is sponsored by DB2 Express
> Download DB2 Express C - the FREE version of DB2 express and take
> control of your XML. No limits. Just data. Click to get it now.
> http://sourceforge.net/powerbar/db2/
> _______________________________________________
> JMLspecs-ESCJava mailing list
> JMLspecs-ESCJava@...
> https://lists.sourceforge.net/lists/listinfo/jmlspecs-escjava

-------------------------------------------------------------------------
This SF.net email is sponsored by DB2 Express
Download DB2 Express C - the FREE version of DB2 express and take
control of your XML. No limits. Just data. Click to get it now.
http://sourceforge.net/powerbar/db2/
_______________________________________________
JMLspecs-ESCJava mailing list
JMLspecs-ESCJava@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-escjava

[Joseph Kiniry]

On 8 Jun, 2007, at 9:40, Dermot Cochran wrote:

>
> On Jun 8, 2007, at 3:03 AM, George Karabotsos wrote:
>
>> Hello all,
>>
>> I am wondering if anyone is working with the ESCTools code in  
>> Eclipse?
>
> Yes, although it needs to be built from the command line using 'make'.

Actually, I only run make (via an Eclipse builder) when I touch the  
AST.  Otherwise, doing builds with Eclipse's autobuild infrastructure  
works fine.  I run overall tests via builders too, but run individual  
unit tests via Eclipse's jUnit integration.

Joe

-------------------------------------------------------------------------
This SF.net email is sponsored by DB2 Express
Download DB2 Express C - the FREE version of DB2 express and take
control of your XML. No limits. Just data. Click to get it now.
http://sourceforge.net/powerbar/db2/
_______________________________________________
JMLspecs-ESCJava mailing list
JMLspecs-ESCJava@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-escjava

[Patrice Chalin-3]

Hi Joe,
> Yup, we all are here at UCD.  And other Mobius partners are starting  
> to do all their development now within Eclipse (many already have  
> been for several months).
>  
Nice.
> We can give you a pre-configured workspace or project if you like.
Is the .project file under CVS not appropriately set?

> It is part of the upcoming public Mobius Program Verification  
> Environment (beta) developer release.
>
> We just distributed pre-release snapshots of all plugins and a  
> developer workspace to Mobius partners this week at the Mobius 2nd  
> annual meeting here in Dublin.
>
> I'll put up the plugins snapshot and workspace snapshot on a private  
> webserver and point you to it.  Sounds good?
>  

Yes it does :).
> Note that we have only tested it all on OS X and Linux at this  
> moment.  If you are a Windows user you'll be our first Windows test  
> subject. :)  We expect it all to "just work", as it did when we moved  
> it to Linux this week for the first time.
>  
George works under Linux. (FYI, Perry go tired of Vista running four
times slower for JDT tests than Linux and so he has switched to Linux
too). So I'll be your Windows/Cygwin guinnea pig.
> Additionally, the new 2.0b1 release of ESC/Java2 runs in a Java 1.5+  
> VM.  And, while it can process 1.5 bytecode,
This is a very welcome enhancement (so I can now switch my default Java
dev env to 1.5).

Cheers,
Patrice

--
Patrice Chalin, ing. jr., Associate Prof., www.encs.concordia.ca/~chalin
Dependable Software Research Group, CSE Department, Concordia University



-------------------------------------------------------------------------
This SF.net email is sponsored by DB2 Express
Download DB2 Express C - the FREE version of DB2 express and take
control of your XML. No limits. Just data. Click to get it now.
http://sourceforge.net/powerbar/db2/
_______________________________________________
JMLspecs-ESCJava mailing list
JMLspecs-ESCJava@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-escjava

[Joseph Kiniry]

On 8 Jun 2007, at 11:58, Patrice Chalin wrote:

> Hi Joe,
>> Yup, we all are here at UCD.  And other Mobius partners are  
>> starting  to do all their development now within Eclipse (many  
>> already have  been for several months).
>>
> Nice.
>> We can give you a pre-configured workspace or project if you like.
> Is the .project file under CVS not appropriately set?

It *should* be.  We'll have to double-check.  Dermot is doing some  
hardware work on his desktop machine this afternoon and we have our  
CASL kick-off today though, so this and the new ESC/Java2 plugin  
release may not happen until early next week.

>> It is part of the upcoming public Mobius Program Verification  
>> Environment (beta) developer release.
>>
>> We just distributed pre-release snapshots of all plugins and a  
>> developer workspace to Mobius partners this week at the Mobius  
>> 2nd  annual meeting here in Dublin.
>>
>> I'll put up the plugins snapshot and workspace snapshot on a  
>> private  webserver and point you to it.  Sounds good?
>>
> Yes it does :).

See
   <http://secure.ucd.ie/~kiniry/mobius/>

>> Note that we have only tested it all on OS X and Linux at this  
>> moment.  If you are a Windows user you'll be our first Windows  
>> test  subject. :)  We expect it all to "just work", as it did when  
>> we moved  it to Linux this week for the first time.
>>
> George works under Linux. (FYI, Perry go tired of Vista running  
> four times slower for JDT tests than Linux and so he has switched  
> to Linux too). So I'll be your Windows/Cygwin guinnea pig.

Ok.

>> Additionally, the new 2.0b1 release of ESC/Java2 runs in a Java 1.5
>> +  VM.  And, while it can process 1.5 bytecode,
> This is a very welcome enhancement (so I can now switch my default  
> Java dev env to 1.5).

Note: only 1.5 *bytecode* is supported at the moment.  We will not  
begin processing 1.5 *sourcecode* until ESC/Java3 is developed later  
this Summer.  But at least you can write 1.4 source in an Eclipse  
running in a 1.5 VM and compile with a 1.5 compiler for the moment.  
It is an excellent transition step because many of the plugins and  
tools we now use require a 1.5 foundation.

Joe



-------------------------------------------------------------------------
This SF.net email is sponsored by DB2 Express
Download DB2 Express C - the FREE version of DB2 express and take
control of your XML. No limits. Just data. Click to get it now.
http://sourceforge.net/powerbar/db2/
_______________________________________________
JMLspecs-ESCJava mailing list
JMLspecs-ESCJava@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-escjava

[Patrice Chalin-3]

Joseph Kiniry wrote:
> It *should* be.  We'll have to double-check.  Dermot is doing some
> hardware work on his desktop machine this afternoon and we have our
> CASL kick-off today though, so this and the new ESC/Java2 plugin
> release may not happen until early next week.
I have made some changes that, hopefully, should resolve the issues
George is having.

How you setup your Eclipse builder to run tests?
> See <http://secure.ucd.ie/~kiniry/mobius/>
Thanks.
> Note: only 1.5 *bytecode* is supported at the moment.
Understood.
>   We will not begin processing 1.5 *sourcecode* until ESC/Java3 is
> developed later this Summer.  But at least you can write 1.4 source in
> an Eclipse running in a 1.5 VM and compile with a 1.5 compiler for the
> moment.  It is an excellent transition step because many of the
> plugins and tools we now use require a 1.5 foundation.
Agreed.

Patrice

--
Patrice Chalin, ing. jr., Associate Prof., www.encs.concordia.ca/~chalin
Dependable Software Research Group, CSE Department, Concordia University



-------------------------------------------------------------------------
This SF.net email is sponsored by DB2 Express
Download DB2 Express C - the FREE version of DB2 express and take
control of your XML. No limits. Just data. Click to get it now.
http://sourceforge.net/powerbar/db2/
_______________________________________________
JMLspecs-ESCJava mailing list
JMLspecs-ESCJava@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-escjava

[Joseph Kiniry]

On 8 Jun 2007, at 13:15, Patrice Chalin wrote:

> Joseph Kiniry wrote:
>> It *should* be.  We'll have to double-check.  Dermot is doing some  
>> hardware work on his desktop machine this afternoon and we have  
>> our CASL kick-off today though, so this and the new ESC/Java2  
>> plugin release may not happen until early next week.
> I have made some changes that, hopefully, should resolve the issues  
> George is having.
> How you setup your Eclipse builder to run tests?

The same way as the builds, via a trivial make call.  We can add  
those builders to the repository too.  Unfortunately I have yet to  
figure out how to convince Eclipse to parse standard GNU command  
output syntax to jump directly to test failure errors and similar.

The C++ feature for Eclipse does have a plugin that does this kind of  
thing, so I think we'll have to figure it out and add it to the  
Mobius PVE in the future to make for more efficient make-based test  
execution.

I'd also like to aggregate all unit tests in a real top-level jUnit  
test suite so that we can avoid using make entirely in the future for  
local ESC/Java(3?) and Mobius PVE testing.  We'll still need make  
though for our planned work in distributed, concurrent testing unit  
and proof testing (under discussion here at UCD).

>> See <http://secure.ucd.ie/~kiniry/mobius/>
> Thanks.

Sure.

>> Note: only 1.5 *bytecode* is supported at the moment.
> Understood.

Great. :)

>>   We will not begin processing 1.5 *sourcecode* until ESC/Java3 is  
>> developed later this Summer.  But at least you can write 1.4  
>> source in an Eclipse running in a 1.5 VM and compile with a 1.5  
>> compiler for the moment.  It is an excellent transition step  
>> because many of the plugins and tools we now use require a 1.5  
>> foundation.
> Agreed.

Fab.

Joe

-------------------------------------------------------------------------
This SF.net email is sponsored by DB2 Express
Download DB2 Express C - the FREE version of DB2 express and take
control of your XML. No limits. Just data. Click to get it now.
http://sourceforge.net/powerbar/db2/
_______________________________________________
JMLspecs-ESCJava mailing list
JMLspecs-ESCJava@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-escjava

[George Karabotsos]

Thank you Joe, I got it working :)

George


-------------------------------------------------------------------------
This SF.net email is sponsored by DB2 Express
Download DB2 Express C - the FREE version of DB2 express and take
control of your XML. No limits. Just data. Click to get it now.
http://sourceforge.net/powerbar/db2/
_______________________________________________
JMLspecs-ESCJava mailing list
JMLspecs-ESCJava@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-escjava

[Patrice Chalin-3]

Joseph Kiniry wrote:

> On 8 Jun 2007, at 13:15, Patrice Chalin wrote:
>> Joseph Kiniry wrote:
>>> It *should* be.  We'll have to double-check.  Dermot is doing some
>>> hardware work on his desktop machine this afternoon and we have our
>>> CASL kick-off today though, so this and the new ESC/Java2 plugin
>>> release may not happen until early next week.
>> I have made some changes that, hopefully, should resolve the issues
>> George is having.
>> How you setup your Eclipse builder to run tests?
> The same way as the builds, via a trivial make call.

But the current "make test" will likely pickup the .class files under
ESCTools/Escjava/classes or ESCTools/Escjava/classfiles whereas Eclipse
puts the .class files that it generates under ESCTools/classfiles.
>   We can add those builders to the repository too.  Unfortunately I
> have yet to figure out how to convince Eclipse to parse standard GNU
> command output syntax to jump directly to test failure errors and similar.
>
> The C++ feature for Eclipse does have a plugin that does this kind of
> thing, so I think we'll have to figure it out and add it to the Mobius
> PVE in the future to make for more efficient make-based test execution.
Good idea -- I've managed to get that to work by using the C/C++ plug-in
(i.e. using the plug-in wholesale, not by borrowing their code).
> I'd also like to aggregate all unit tests in a real top-level jUnit
> test suite so that we can avoid using make entirely in the future for
> local ESC/Java(3?) and Mobius PVE testing.  We'll still need make
> though for our planned work in distributed, concurrent testing unit
> and proof testing (under discussion here at UCD).
Sounds good.

Cheers,
Patrice

--
Patrice Chalin, ing. jr., Associate Prof., www.encs.concordia.ca/~chalin
Dependable Software Research Group, CSE Department, Concordia University



-------------------------------------------------------------------------
This SF.net email is sponsored by DB2 Express
Download DB2 Express C - the FREE version of DB2 express and take
control of your XML. No limits. Just data. Click to get it now.
http://sourceforge.net/powerbar/db2/
_______________________________________________
JMLspecs-ESCJava mailing list
JMLspecs-ESCJava@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-escjava

[Joseph Kiniry]

On 8 Jun, 2007, at 20:36, Patrice Chalin wrote:

> Joseph Kiniry wrote:
>> On 8 Jun 2007, at 13:15, Patrice Chalin wrote:
>>> Joseph Kiniry wrote:
>>>> It *should* be.  We'll have to double-check.  Dermot is doing  
>>>> some hardware work on his desktop machine this afternoon and we  
>>>> have our CASL kick-off today though, so this and the new ESC/
>>>> Java2 plugin release may not happen until early next week.
>>> I have made some changes that, hopefully, should resolve the  
>>> issues George is having.
>>> How you setup your Eclipse builder to run tests?
>> The same way as the builds, via a trivial make call.
> But the current "make test" will likely pickup the .class files  
> under ESCTools/Escjava/classes or ESCTools/Escjava/classfiles  
> whereas Eclipse puts the .class files that it generates under  
> ESCTools/classfiles.

I just tell Eclipse to build into Escjava/classes and make sure it is  
at the front of the classpath during the tests.

>>   We can add those builders to the repository too.  Unfortunately  
>> I have yet to figure out how to convince Eclipse to parse standard  
>> GNU command output syntax to jump directly to test failure errors  
>> and similar.
>>
>> The C++ feature for Eclipse does have a plugin that does this kind  
>> of thing, so I think we'll have to figure it out and add it to the  
>> Mobius PVE in the future to make for more efficient make-based  
>> test execution.
> Good idea -- I've managed to get that to work by using the C/C++  
> plug-in (i.e. using the plug-in wholesale, not by borrowing their  
> code).

Oh?  How did you do that?  I was unable to install the plugin  
independently on my first attempt many moons ago before I understand  
Eclipse plugins and features well.  Was it really not a problem?

>> I'd also like to aggregate all unit tests in a real top-level  
>> jUnit test suite so that we can avoid using make entirely in the  
>> future for local ESC/Java(3?) and Mobius PVE testing.  We'll still  
>> need make though for our planned work in distributed, concurrent  
>> testing unit and proof testing (under discussion here at UCD).
> Sounds good.

Great.

Joe

-------------------------------------------------------------------------
This SF.net email is sponsored by DB2 Express
Download DB2 Express C - the FREE version of DB2 express and take
control of your XML. No limits. Just data. Click to get it now.
http://sourceforge.net/powerbar/db2/
_______________________________________________
JMLspecs-ESCJava mailing list
JMLspecs-ESCJava@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-escjava