jmlspecs-developers — Discussions among JML developers; includes tracker report changes

[Jmlspecs-developers] Practitioners' Thoughts on the Requirements Engineering

[Mert O. <ozk...@gm...>]

Dear Sir or Madam,


We prepared a short survey to understand practitioners’ perspectives
towards the requirements engineering. Our survey basically aims to clarify
on many aspects of the requirements engineering applied in industry, including
(i) requirements gathering and specifications, (ii) requirements
modifications, (iii) requirements analysis, and (iv) requirements
transformation. The survey results will be submitted to a reputable journal
on software engineering.


The survey takes about 2-10 minutes to participate, we would be so grateful
if you could separate your time. Also, please circulate the e-mail to
anyone who may be interested in.


The survey link: https://forms.gle/DhLqr15GXVhJhzzy6


All the best,

Dr. Mert Ozkaya

[Jmlspecs-developers] Practitioners' Expectations from Language Workbenches

[Mert O. <ozk...@gm...>]

Dear Practitioner,


We have recently released a survey on understanding the expectations of
practitioners in different industries from the meta-modeling tools (aka
language workbenches) for the (domain-specific) language development. The
survey also aims to learn the top-used meta-modeling tools in industry and
the challenges that practitioners face with.



The survey is accessible via the link:
https://docs.google.com/forms/d/e/1FAIpQLScJK_qyKpFW18qv2Yf11Qsduq157jnc0bkmpRfMUOdH6v6Jgw/viewform?usp=sf_link



The survey takes 3-13 minutes at most, and your contribution to
the survey is extremely valuable and highly needed. Can you please support
our research by filling in the survey and forwarding the survey to any of
your stakeholders whom you think may wish to participate in the survey ?



The survey results will be made available online and published as a
scientific journal/conference paper.

Best Regards,
Dr. Mert Ozkaya

[Jmlspecs-developers] The Challenges that Practitioners face with on Software Modeling

[Mert O. <ozk...@gm...>]

Dear All,

We have recently released a survey on understanding the challenges that
practitioners face with in their software modeling activities. The survey
takes approximately 2-5 minutes to complete.

We would be so grateful if you could separate a few minutes of you to
participate in our research.

The survey link:
https://docs.google.com/forms/d/e/1FAIpQLScwFMKoOJHDYF6GDETWh5H2w3W57G78Fb2SF0ABM9uTthN_hQ/viewform?usp=sf_link
<https://docs.google.com/forms/d/e/1FAIpQLScwFMKoOJHDYF6GDETWh5H2w3W57G78Fb2SF0ABM9uTthN_hQ/viewform?usp=sf_link>

Best,
Dr. Mert Ozkaya

[Jmlspecs-developers] What Industry Wants from Academia in Software Modeling

[Mert O. <ozk...@gm...>]

Dear All,

As we have circulated recently, we have been conducting a survey on
understanding the challenges that practitioners face with in their software
modeling activities. While the survey is intended for answering some
crucial questions that have been clearly addressed so far (e.g., what types
of challenges are more popular in different industries, the concrete
challenges that practitioners frequently face with, and what do
practitioners expect from academia), we have not managed to attract as many
participants as expected.

We would be grateful if you can separate 2-5 minutes of you to fill in the
survey questions. Indeed, we will write a journal paper that discusses the
survey results once a sufficient amount of participants contributed.

The Survey Link:
https://docs.google.com/forms/d/e/1FAIpQLScwFMKoOJHDYF6GDETWh5H2w3W57G78Fb2SF0ABM9uTthN_hQ/viewform?usp=sf_link
<https://docs.google.com/forms/d/e/1FAIpQLScwFMKoOJHDYF6GDETWh5H2w3W57G78Fb2SF0ABM9uTthN_hQ/viewform?usp=sf_link>

Please do not hesitate to contact me about the survey.

We are looking forward to receiving your invaluable contributions (just 2-5
mins).

Best regards,
Mert

[Jmlspecs-developers] What Industry Wants from Academia in Software Modeling

[Mert O. <ozk...@gm...>]

Dear All,

We have recently released a survey on understanding the challenges that
practitioners face with about software modeling and the particular problems
that practitioners wish the researchers in academia to deal with.

The survey is accessible via the link:
https://docs.google.com/forms/d/e/1FAIpQLScwFMKoOJHDYF6GDETWh5H2w3W57G78Fb2SF0ABM9uTthN_hQ/viewform?usp=sf_link

The survey takes 2-7 minutes at most, and your contribution to the survey
is extremely valuable and highly needed. Can you please support our
research by filling in the survey?

The survey results will be made available online and published as a
scientific journal/conference paper.

Best,
Mert
--
Dr. Mert Ozkaya
Department of Computer Engineering,
Yeditepe University,
Istanbul - Turkey
Tel: 0090 216 578 04 20 Ext: 1424
Fax: 0090 216 578 04 00
URL: http://cse.yeditepe.edu.tr/~mozkaya

Re: [Jmlspecs-developers] Is OpenJML open source?

[Gary T. L. <le...@ee...>]

Hi Zhi,

Yes, the source code is in sourceforge.net. See
http://sourceforge.net/p/jmlspecs/wiki/OpenJmlSetup/ for details.

On Thu, Feb 26, 2015 at 1:36 PM, <zh...@gm...> wrote:

> Hi,
>
> I cannot seem to find the source repository. Is it an open source project?
>
> Thanks
>
> Zhi
>
>
> ------------------------------------------------------------------------------
> Dive into the World of Parallel Programming The Go Parallel Website,
> sponsored
> by Intel and developed in partnership with Slashdot Media, is your hub for
> all
> things parallel software development, from weekly thought leadership blogs
> to
> news, videos, case studies, tutorials and more. Take a look and join the
> conversation now. http://goparallel.sourceforge.net/
> _______________________________________________
> Jmlspecs-developers mailing list
> Jml...@li...
> https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers
>
>


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

[Jmlspecs-developers] Is OpenJML open source?

[<zh...@gm...>]

Hi,

I cannot seem to find the source repository. Is it an open source project?

Thanks

Zhi

[Jmlspecs-developers] Help Improve OpenJML By Taking Part in the "State of OpenJML" Survey!

[John L. S. <jl...@cs...>]

Hello,

 

My name is John L. Singleton and I am a Ph.D. student working in the Formal
Methods Lab at the University of Central Florida. I am writing to ask you
all to join me in taking part in a survey designed to help us improve
OpenJML. This survey covers issues such as installation, features, user
experience, and documentation. Our goal is to highlight the areas where
OpenJML is doing great, and to identify the areas we can improve. 

 

As members of the OpenJML community, we would highly value any feedback you
could provide. All feedback will of course be anonymous and only used for
the purposes of this analysis. The results of this survey will be presented
at the upcoming conference: JML: Advancing Specification Language
Methodologies, to take place in at the Lorentz Center in Leiden. 

 

I want to thank you in advance for taking the time to answer this survey! We
look forward to hearing your thoughts! 

 

Take the survey, here:
https://qtrial2015az1.az1.qualtrics.com/SE/?SID=SV_cGs0GIz18WUtwVv

 

Best,

JLS

 

[Jmlspecs-developers] JML Wiki moved

[Gary T. L. <le...@ee...>]

Hi,

I discovered today that on sourceforge.net, the jmlspecs project wiki was
no longer accessible. Apparently about a week ago the trac wikis were
removed. But I submitted a support ticket and the problem has already been
fixed. Thus the effect of this is that the JML wiki has been moved to:

https://sourceforge.net/p/jmlspecs/wiki/Home/

I will update the links from the jmlspecs.org website as soon as I can
(today).

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

[Jmlspecs-developers] JML's Bright Future -- with your help!

[Gary T. L. <le...@ee...>]

Hi,

At the Shonan workshop on JML this month (May 2013) I made some statements
about the future of JML. I thought I would share them more generally here
in order to ask for your help in making the future of JML bright indeed.
 Think of this as my "manifesto on JML".

A core belief I have is that Java will be important for a long time and
that by working together all the participants in the JML project can lower
costs for users and maximize user benefits.
The advantage of JML is that it acts as "glue" for formal methods tools and
lets users apply many different tools to a single specified piece of code.

I characterize *the mission of the JML effort *as:

   - To make formal methods for Java practical and useful, and
   - To enhance our individual reputations and careers.

The JML project has been very successful, but those successes were largely
due to having useful tools. In that respect I believe more strongly now
that the way forward for JML is through the OpenJML platform, and I urge
all reading this to work towards the success of OpenJML.

Currently JML is in the "Decline or Revival" state of its life cycle,
having reached Maturity around 2007 or so. (These stages are from Wynn's
paper "Organizational Structure of Open Source Projects: A Life Cycle
Approach," 7th Annual Conference of the Southern Association for
Information Systems, Georgia, 2003.)

As I did at the Shonan meeting, I commit myself to JML's revival and I ask
for your help. I have been and will continue to work on the JML Reference
Manual. If you have interests in writing a textbook that uses JML for
teaching CS2 (data structures in Java), please let me know and we can
coordinate on that.  (The need for such a textbook was pointed out in the
education discussion at the workshop.)

I would also like to see volunteers from the JML community to work on the
following topics:

   - Maintain parts of the JML web site
   - Test OpenJML and provide bug reports
   - Submit patches for bugs
   - Provide (shell) scripts, packaging for OpenJML

(Marieke Huismann has already volunteered to work on the education portion
of the web site. John Singleton has started testing OpenJML and providing
bug reports.)

Even if you can't get involved in such efforts personally, please urge your
students to get involved in:

   - Testing and filing bug reports on OpenJML, and
   - Submitting patches for bugs.

It would be great if someone would volunteer speahead the efforts to grow
the JML community with new developers. The job of such a person (or
committee) would be: to recruit such students, to coordinate documentation
about OpenJML, to cooperate with David Cok to carve out pieces of OpenJML
for the most promising volunteers (with a view towards making them active
developers), and to publicly reward and encourage volunteers.

Thanks for reading. I know that with your help we can make the future of
JML bright indeed.

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

Re: [Jmlspecs-developers] Fwd: SourceForge Repo Clone Complete

[Gary T. L. <le...@ee...>]

Hi all,

I'm willing to look into migrating the wiki, once sourceforge.net tells us
how to do that (or when I can find time).


On Tue, Nov 27, 2012 at 11:55 PM, co...@fr...
<co...@fr...>wrote:

>
>
>   ------------------------------
> Gary,
>
> The tickets (bug-tracking) system is remaining, I believe. However as you
> say trac is going away. There is material there about JML, OpenJML, and
> other JML-related projects in wiki format.
> There is a built-in wiki system for sourceforge. I expect that eventually
> sourceforge will tell us how to migrate from trac to the sourceforge wiki.
> The
>
>
> https://sourceforge.net/p/forge/community-docs/Migrating%20Trac%20from%20Hosted%20Apps/
>
> page appears incomplete (as well as a lengthy set of steps to follow).
> Perhaps there are few enough pages they could be transferred manually.
>
> Anyone else have experience with sourceforge migration? and trac to wiki
> migration?
>
> - David
>
> *
>
>
> From:* Gary T. Leavens <le...@ee...>
> *To:* "co...@fr..." <co...@fr...>
> *Sent:* Tuesday, November 27, 2012 9:31 PM
> *Subject:* Re: [Jmlspecs-developers] Fwd: SourceForge Repo Clone Complete
>
> Hi David,
>
> Sorry for the extra trouble. I'm not sure what to do about labels and
> tickets. Apparently sourceforge is going to discontinue use of trac soon,
> so we'll have to figure out what to do about that. Are you using trac?
>
>


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

[Jmlspecs-developers] MultiJava site

[Werner D. <wd...@ya...>]

The domain:

http://multijava.org/


has expired at least a few months ago (or at least I understand its website less now ;-) )
The SourceForge sites at:

http://multijava.sourceforge.net/

http://multijava.sf.net/


still work.
There are a few dangling references on the JML website.

FYI,
cu, WMD.

Re: [Jmlspecs-developers] Fwd: SourceForge Repo Clone Complete

[<co...@fr...>]

________________________________
 Gary,

The tickets (bug-tracking) system is remaining, I believe. However as you say trac is going away. There is material there about JML, OpenJML, and other JML-related projectsin wiki format.
There is a built-in wiki system for sourceforge. I expect that eventually sourceforge will tell us how to migrate from trac tothe sourceforge wiki. The

https://sourceforge.net/p/forge/community-docs/Migrating%20Trac%20from%20Hosted%20Apps/

page appears incomplete (as well as a lengthy set of steps to follow).
Perhaps there are few enough pages they could be transferred manually.

Anyone else have experience with sourceforge migration? and trac to wiki migration?

- David




From: Gary T. Leavens <le...@ee...>
To: "co...@fr..." <co...@fr...> 
Sent: Tuesday, November 27, 2012 9:31 PM
Subject: Re: [Jmlspecs-developers] Fwd: SourceForge Repo Clone Complete
 

Hi David,

Sorry for the extra trouble. I'm not sure what to do about labels and tickets. Apparently sourceforge is going to discontinue use of trac soon, so we'll have to figure out what to do about that. Are you using trac?

Re: [Jmlspecs-developers] Fwd: SourceForge Repo Clone Complete

[<co...@fr...>]

Thanks Gary - though with a slight warning I could have avoided being caught in the middle of some work - but I think I can recover.

Regarding tracker tickets, it appears the only way to distinguish different subprojects is using the "labels" field.
So anything I find that is OpenJML related I'm adding an 'OpenJML' label - others please do the same


One can search on labels, but

- I don't see a way to display labels in lists of tickets
- nor a way to block edit the labels of a set of tickets

(If I'm missing something, please let me know, as it would save time)

- David



________________________________
 From: Gary T. Leavens <le...@ee...>
To: JML developers list <jml...@li...> 
Sent: Tuesday, November 27, 2012 6:05 PM
Subject: [Jmlspecs-developers] Fwd: SourceForge Repo Clone Complete
 

Hi all,

Apparently at sourceforge.net, there is a new URL to use for SVN checkouts of the jmlspecs repositories. See below and substitute your sourceforge.net username for "leavens".


---------- Forwarded message ----------
From: SourceForge.net <nor...@in...>
Date: Tue, Nov 27, 2012 at 5:45 PM
Subject: SourceForge Repo Clone Complete
To: no...@in...



Your cloned repository code in project jmlspecs is now ready for use.
Old repository url: http://jmlspecs.svn.sourceforge.net/svnroot/jmlspecs 
New repository checkout command: svn checkout --username=leavens svn+ssh://le...@sv.../p/jmlspecs/code/trunk jmlspecs-code 
You and any other developers should do a fresh checkout using the new repository location.


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

------------------------------------------------------------------------------
Keep yourself connected to Go Parallel: 
DESIGN Expert tips on starting your parallel project right.
http://goparallel.sourceforge.net
_______________________________________________
Jmlspecs-developers mailing list
Jml...@li...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers

[Jmlspecs-developers] Fwd: SourceForge Repo Clone Complete

[Gary T. L. <le...@ee...>]

Hi all,

Apparently at sourceforge.net, there is a new URL to use for SVN checkouts
of the jmlspecs repositories. See below and substitute your
sourceforge.netusername for "leavens".

---------- Forwarded message ----------
From: SourceForge.net <nor...@in...>
Date: Tue, Nov 27, 2012 at 5:45 PM
Subject: SourceForge Repo Clone Complete
To: no...@in...


Your cloned repository code in project jmlspecs is now ready for use.

Old repository url: http://jmlspecs.svn.sourceforge.net/svnroot/jmlspecs

New repository checkout command: svn checkout --username=leavens svn+ssh://
le...@sv.../p/jmlspecs/code/trunk jmlspecs-code

You and any other developers should do a fresh checkout using the new
repository location.



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

[Jmlspecs-developers] Fwd: SourceForge Project Upgrade Notification

[Gary T. L. <le...@ee...>]

Hi,

The JMLspecs and MultiJava projects have both been upgraded on
Sourceforge.net to their new system. Apparently this might cause some
problems accessing the code repositories for a while. See below for more
details.

---------- Forwarded message ----------
From: SourceForge.net <nor...@in...>
Date: Tue, Nov 27, 2012 at 2:45 PM
Subject: SourceForge Project Upgrade Notification
To: no...@in...


Your project, Java Modeling Language (JML), has been upgraded.

Your source code repositories are currently being migrated to the new
setup. You will receive another email when that import is complete. That
means that you and any other developers should do a fresh checkout using
the new repository location when it is ready (see the "code" tab). Please
be aware that large repositories may take a long time.

Please report any issues to us at
https://sourceforge.net/p/forge/site-support/new/  Thanks!



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

[Jmlspecs-developers] [ jmlspecs-Bugs-3582756 ] openjml rac extended class

[SourceForge.net <no...@so...>]

Bugs item #3582756, was opened at 2012-11-02 16:22
Message generated for change (Tracker Item Submitted) made by fithwith
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=510629&aid=3582756&group_id=65346

Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: OpenJML
Group: latest release
Status: Open
Resolution: None
Priority: 5
Private: No
Submitted By: fithwith (fithwith)
Assigned to: David Cok (davidcok)
Summary: openjml rac extended class

Initial Comment:
hi all,
my config is:
-eclipse juno
-openjml eclipse plugin v 0.2.7

i have two class Person and Child when i want rac class Child an error occur but no error with Person class, the rac of Person class works perfectly

so my probleme is with Child class, i did some test and i noticed that when i delete "extends Parent" from child class the rac works perfectly

the error:

INVALID COMMAND LINE: return code = 4   Command: -rac -d F:/Dev_Project/eclipse/JMLTest/bin -source 1.7 -noPurityCheck -showNotImplemented -noInternalSpecs -noInternalRuntime -nonnullByDefault -specspath ;F:\eclipse\configuration\org.eclipse.osgi\bundles\950\2\.cp\java7;F:\eclipse\configuration\org.eclipse.osgi\bundles\950\2\.cp\java6;F:\eclipse\configuration\org.eclipse.osgi\bundles\950\2\.cp\java5;F:\eclipse\configuration\org.eclipse.osgi\bundles\950\2\.cp\java4 -classpath F:/Dev_Project/eclipse/JMLTest/src;C:/Program Files/Java/jre7/lib/resources.jar;C:/Program Files/Java/jre7/lib/rt.jar;C:/Program Files/Java/jre7/lib/jsse.jar;C:/Program Files/Java/jre7/lib/jce.jar;C:/Program Files/Java/jre7/lib/charsets.jar;C:/Program Files/Java/jre7/lib/jfr.jar;C:/Program Files/Java/jre7/lib/ext/access-bridge-64.jar;C:/Program Files/Java/jre7/lib/ext/dnsns.jar;C:/Program Files/Java/jre7/lib/ext/jaccess.jar;C:/Program Files/Java/jre7/lib/ext/localedata.jar;C:/Program Files/Java/jre7/lib/ext/sunec.jar;C:/Program Files/Java/jre7/lib/ext/sunjce_provider.jar;C:/Program Files/Java/jre7/lib/ext/sunmscapi.jar;C:/Program Files/Java/jre7/lib/ext/zipfs.jar;F:/eclipse/plugins/org.jmlspecs.OpenJMLUI_0.2.7/jmlruntime.jar;/;F:\eclipse\plugins\org.jmlspecs.OpenJMLUI_0.2.7\bin\..\jmlruntime.jar -dirs F:/Dev_Project/eclipse/JMLTest/src/PersonChild/Child.java 


----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=510629&aid=3582756&group_id=65346

[Jmlspecs-developers] [ jmlspecs-Support Requests-3541932 ] Problem accessing ghost fields via the API

[SourceForge.net <no...@so...>]

Support Requests item #3541932, was opened at 2012-07-09 23:41
Message generated for change (Tracker Item Submitted) made by jseiter
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=510630&aid=3541932&group_id=65346

Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: Debugging
Group: None
Status: Open
Priority: 5
Private: No
Submitted By: Julia Seiter (jseiter)
Assigned to: Gary T. Leavens (leavens)
Summary: Problem accessing ghost fields via the API

Initial Comment:
Hello,

I am working with OpenJML at the moment in order to transform Java + JML code into a different model. However, trying to process ghost and model fields through the OpenJML-API I experience some difficulties. What I do is the following:
- create a new API
- use parseSingleFile to process the input
- apply checkAndEnter to the resulting JMLCompilationUnit
The application of checkAndEnter leads to the following error message:

error: cannot find symbol
	/*@ ensures this.b == c;
	                      ^
  symbol:   variable c
  location: class ArrayOps

where c is declared as: /*@ ghost ArrayOps c;
I am also getting a NullPointerException. Unfortunately, I couldn't figure out on my own where this error is originated. Without the call of checkAndEnter, I am getting different error messages later on when I'm trying to use the variable c in my JML code.

I am wondering if I am using the API incorrectly or if there is something wrong with the ghost variable I declared?

Thank you for your help,
Julia

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=510630&aid=3541932&group_id=65346

[Jmlspecs-developers] [ jmlspecs-Support Requests-3512783 ] Source-code download problem

[SourceForge.net <no...@so...>]

Support Requests item #3512783, was opened at 2012-03-29 04:30
Message generated for change (Tracker Item Submitted) made by mertozkaya
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=510630&aid=3512783&group_id=65346

Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: Installation problem
Group: None
Status: Open
Priority: 5
Private: No
Submitted By: mert (mertozkaya)
Assigned to: Gary T. Leavens (leavens)
Summary: Source-code download problem

Initial Comment:
Hi All,
I have just registered for the Sourceforge for the purpose of checking out JML source-codes from the cvs repository,
However, once I have attempted to checkout and subsequently been asked to type password, my sourceforge password was not accepted.
I guess that this is because someone need to register me as one of the developers. Would you please help on this regard so that I can start working on the 
source-codes ?

Thanks,
Mert

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=510630&aid=3512783&group_id=65346

[Jmlspecs-developers] [ jmlspecs-Support Requests-3428104 ] Using RAC and ESC

[SourceForge.net <no...@so...>]

Support Requests item #3428104, was opened at 2011-10-25 10:41
Message generated for change (Tracker Item Submitted) made by peteryhwong
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=510630&aid=3428104&group_id=65346

Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: Can't figure out how to use working  tool
Group: None
Status: Open
Priority: 5
Private: No
Submitted By: Peter Wong (peteryhwong)
Assigned to: Nobody/Anonymous (nobody)
Summary: Using RAC and ESC

Initial Comment:
I am experimenting with ESC and RAC features provided by OpenJML. However, I come to some issues with using these features.

For ESC, I use the following command, where the corresponding OpenJML jar files are downloaded from http://jmlspecs.sourceforge.net/openjml.tar.gz and yices is obtained from http://yices.csl.sri.com/cgi-bin/yices-newlicense.cgi?file=yices-1.0.31-x86_64-pc-linux-gnu-static-gmp.tar.gz

/usr/java/jdk1.7.0/bin/java -Dopenjml.defaultProver=yices -Dopenjml.prover.yices=<path to yices executable> -jar <path-to-openjml.jar> -noPurityCheck -specspath <path-to-jmlspec.jar> -noInternalSpecs -noInternalRuntime -cp <path-to-jmlruntimejar> -dir <dir-of-C.java> -command esc

I get the following 

Internal JML bug - please report.  BuildOpenJML-20111005
java.lang.NoClassDefFoundError: org/smtlib/IVisitor$VisitorException
	at org.jmlspecs.openjml.JmlCompiler.esc(JmlCompiler.java:482)
	at org.jmlspecs.openjml.JmlCompiler.desugar(JmlCompiler.java:346)
	at com.sun.tools.javac.main.JavaCompiler.desugar(JavaCompiler.java:1280)
	at com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:866)
	at org.jmlspecs.openjml.JmlCompiler.compile2(JmlCompiler.java:527)
	at com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:835)
	at com.sun.tools.javac.main.Main.compile(Main.java:417)
	at com.sun.tools.javac.main.Main.compile(Main.java:331)
	at org.jmlspecs.openjml.Main.compile(Main.java:367)
	at com.sun.tools.javac.main.Main.compile(Main.java:322)
	at org.jmlspecs.openjml.Main.execute(Main.java:322)
	at org.jmlspecs.openjml.Main.execute(Main.java:288)
	at org.jmlspecs.openjml.Main.execute(Main.java:275)
	at org.jmlspecs.openjml.Main.main(Main.java:248)
Caused by: java.lang.ClassNotFoundException: org.smtlib.IVisitor$VisitorException
	at java.net.URLClassLoader$1.run(URLClassLoader.java:366)
	at java.net.URLClassLoader$1.run(URLClassLoader.java:355)
	at java.security.AccessController.doPrivileged(Native Method)
	at java.net.URLClassLoader.findClass(URLClassLoader.java:354)
	at java.lang.ClassLoader.loadClass(ClassLoader.java:423)
	at sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:308)
	at java.lang.ClassLoader.loadClass(ClassLoader.java:356)
	... 14 more

If I run RAC I use the following command where OpenJML and Yices are obtained from the same places as indicated above

/usr/java/jdk1.7.0/bin/java -Dopenjml.defaultProver=yices -Dopenjml.prover.yices=<path to yices executable> -jar <path-to-openjml.jar> -noPurityCheck -specspath <path-to-jmlspec.jar> -noInternalSpecs -noInternalRuntime -cp <path-to-jmlruntimejar> -dir <dir-of-C.java> -command rac

and get the following error

Internal JML bug - please report.  BuildOpenJML-20111005
java.lang.NullPointerException
	at com.sun.tools.javac.comp.JmlRac.visitMethodDef(JmlRac.java:2508)
	at com.sun.tools.javac.comp.JmlRac.visitJmlMethodDecl(JmlRac.java:2638)
	at org.jmlspecs.openjml.JmlTree$JmlMethodDecl.accept(JmlTree.java:1040)
	at com.sun.tools.javac.tree.TreeTranslator.translate(TreeTranslator.java:58)
	at com.sun.tools.javac.tree.TreeTranslator.translate(TreeTranslator.java:70)
	at com.sun.tools.javac.tree.TreeTranslator.visitClassDef(TreeTranslator.java:134)
	at com.sun.tools.javac.comp.JmlRac.visitClassDef(JmlRac.java:1428)
	at com.sun.tools.javac.comp.JmlRac.visitJmlClassDecl(JmlRac.java:1491)
	at org.jmlspecs.openjml.JmlTree$JmlClassDecl.accept(JmlTree.java:986)
	at com.sun.tools.javac.tree.TreeTranslator.translate(TreeTranslator.java:58)
	at org.jmlspecs.openjml.JmlCompiler.rac(JmlCompiler.java:452)
	at org.jmlspecs.openjml.JmlCompiler.desugar(JmlCompiler.java:352)
	at com.sun.tools.javac.main.JavaCompiler.desugar(JavaCompiler.java:1280)
	at com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:866)
	at org.jmlspecs.openjml.JmlCompiler.compile2(JmlCompiler.java:527)
	at com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:835)
	at com.sun.tools.javac.main.Main.compile(Main.java:417)
	at com.sun.tools.javac.main.Main.compile(Main.java:331)
	at org.jmlspecs.openjml.Main.compile(Main.java:367)
	at com.sun.tools.javac.main.Main.compile(Main.java:322)
	at org.jmlspecs.openjml.Main.execute(Main.java:322)
	at org.jmlspecs.openjml.Main.execute(Main.java:288)
	at org.jmlspecs.openjml.Main.execute(Main.java:275)
	at org.jmlspecs.openjml.Main.main(Main.java:248)

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=510630&aid=3428104&group_id=65346

[Jmlspecs-developers] [ jmlspecs-Bugs-3421186 ] OpenJML does not properly type check enum definition

[SourceForge.net <no...@so...>]

Bugs item #3421186, was opened at 2011-10-10 15:51
Message generated for change (Tracker Item Submitted) made by peteryhwong
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=510629&aid=3421186&group_id=65346

Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: None
Group: None
Status: Open
Resolution: None
Priority: 5
Private: No
Submitted By: Peter Wong (peteryhwong)
Assigned to: Nobody/Anonymous (nobody)
Summary: OpenJML does not properly type check enum definition

Initial Comment:
Given 

{{{
public enum X { Y; X() { } }
}}}

The most recent OpenJML build (BuildOpenJML-20111005)  erroneously gives the following type error.

{{{
X.java:5: error: The method <init> in the specification matches a Java method X() with different modifiers: private
	X() { }
	^
}}}

This relates to 'OpenJML does not properly type check enum definition - ID: 3366092'. 

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=510629&aid=3421186&group_id=65346

[Jmlspecs-developers] [ jmlspecs-Bugs-3421143 ] type checker throws an AssertionError when typechecking enum

[SourceForge.net <no...@so...>]

Bugs item #3421143, was opened at 2011-10-10 13:57
Message generated for change (Tracker Item Submitted) made by peteryhwong
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=510629&aid=3421143&group_id=65346

Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: OpenJML
Group: latest release
Status: Open
Resolution: None
Priority: 5
Private: No
Submitted By: Peter Wong (peteryhwong)
Assigned to: David Cok (davidcok)
Summary: type checker throws an AssertionError when typechecking enum

Initial Comment:
JML throws an AssertionError when typechecking the following enum type

{{{
public enum X { 
	Y;
	public X m() {
		for (X c : values()) break; 
		return Y;
	}
}
}}}

The stack trace is as follows:

{{{
java.lang.AssertionError
	at com.sun.tools.javac.util.Assert.error(Assert.java:126)
	at com.sun.tools.javac.util.Assert.check(Assert.java:45)
	at com.sun.tools.javac.comp.Flow.visitMethodDef(Flow.java:768)
	at com.sun.tools.javac.comp.JmlFlow.visitJmlMethodDecl(JmlFlow.java:126)
	at org.jmlspecs.openjml.JmlTree$JmlMethodDecl.accept(JmlTree.java:1040)
	at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49)
	at com.sun.tools.javac.comp.Flow.visitClassDef(Flow.java:698)
	at com.sun.tools.javac.comp.JmlFlow.visitJmlClassDecl(JmlFlow.java:148)
	at org.jmlspecs.openjml.JmlTree$JmlClassDecl.accept(JmlTree.java:986)
	at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49)
	at com.sun.tools.javac.comp.Flow.analyzeTree(Flow.java:1469)
	at com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1251)
	at org.jmlspecs.openjml.JmlCompiler.flow(JmlCompiler.java:394)
	at com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1215)
	at com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:866)
	at org.jmlspecs.openjml.JmlCompiler.compile2(JmlCompiler.java:527)
	at com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:835)
	at com.sun.tools.javac.main.Main.compile(Main.java:417)
	at com.sun.tools.javac.main.Main.compile(Main.java:331)
	at org.jmlspecs.openjml.Main.compile(Main.java:367)
	at com.sun.tools.javac.main.Main.compile(Main.java:322)
	at org.jmlspecs.openjml.Main.execute(Main.java:322)
	at org.jmlspecs.openjml.Main.execute(Main.java:288)
	at org.jmlspecs.openjml.Main.execute(Main.java:275)
	at org.jmlspecs.openjml.Main.main(Main.java:248)
}}}

Note that this error can be eliminated with the keyword 'break' is removed.

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=510629&aid=3421143&group_id=65346

Re: [Jmlspecs-developers] [Jmlspecs-releases] Release of OpenJML 0.2.1

[Gary T. L. <le...@ee...>]

Hi Magne,

It's true, that tool activities haven't been progressing as fast as we
would like, and also the web page hasn't been updated as often as I
might like. The latter is partly due to me taking over the position of
interim chair of my department for the past year.

David Cok has been leading efforts to make a new version of  the JML
tools that is based on OpenJDK (and thus is up to date) and also has
plans to make that work in Eclipse. If you or others you know would
like to contribute to that effort, we'd be glad to have your help.

On Mon, Sep 19, 2011 at 9:09 AM, Magne Haveraaen
<Mag...@ii...> wrote:
> Hi Gary,
>
> there does not seem to be too much activity on JML for the past few years,
> and the http://www.cs.ucf.edu/~leavens/JML/ also gives a slightly dated
> feeling.
>
> The problem is that I am looking for an Eclipse plugin that would support
> JML for Java 6 (or newer), with asserts, generics, new style for loops etc.
>
> Does this exist - or is anybody active in creating such a plugin and tool?
>
> Magne
>
> --
> Magne Haveraaen
> https://www.ii.uib.no/~magne/
> http://bldl.ii.uib.no/
>
>
>
>



-- 
        Gary T. Leavens
        437D Harris Center (Bldg. 116)
        Dept. 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
        le...@ee...

[Jmlspecs-developers] [ jmlspecs-Bugs-3388690 ] Placing Model Field in Own Datagroup Causes Stack Overflow

[SourceForge.net <no...@so...>]

Bugs item #3388690, was opened at 2011-08-08 16:15
Message generated for change (Tracker Item Submitted) made by dmzimmerman
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=510629&aid=3388690&group_id=65346

Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: OpenJML
Group: None
Status: Open
Resolution: None
Priority: 6
Private: No
Submitted By: Daniel M. Zimmerman (dmzimmerman)
Assigned to: David Cok (davidcok)
Summary: Placing Model Field in Own Datagroup Causes Stack Overflow

Initial Comment:
The attached code, which declares a model field called "height" and explicitly places it in a datagroup called "height" (its own implicit datagroup, into which it is placed when created in any event), causes the OpenJML compiler to fail with a stack overflow error. The same code compiles without incident by the JML2 compiler, which seems to just ignore the extra datagroup placement. Changing the offending "in" to "in_redundantly" does not change the result, but removing it entirely does allow OpenJML to compile the code.

(I have left the offending "in" as "in_redundantly" to make it obvious in the attached code)

The code also will crash the OpenJML compiler when RAC compiled, but since data groups are not yet supported in RAC, that is (I guess) expected.

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=510629&aid=3388690&group_id=65346

[Jmlspecs-developers] [ jmlspecs-Bugs-3377329 ] Internal Error when compiling foreach loops

[SourceForge.net <no...@so...>]

Bugs item #3377329, was opened at 2011-07-25 19:02
Message generated for change (Tracker Item Submitted) made by hoenicke
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=510629&aid=3377329&group_id=65346

Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: OpenJML
Group: None
Status: Open
Resolution: None
Priority: 5
Private: No
Submitted By: Jochen Hoenicke (hoenicke)
Assigned to: David Cok (davidcok)
Summary: Internal Error when compiling foreach loops

Initial Comment:
It looks like continue and break statements in foreach loops cause an internal failure.
See the attached file.  The method test1 works fine, on test2 it crashes.

Versions
OpenJMLUI_0.2.1 eclipse plugin
Java 1.7.0
Eclipse 3.7.0


----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=510629&aid=3377329&group_id=65346