Method Specification Inconsistency #481

samanthasyeda · 2016-11-02T21:55:04Z

Hi All,

I have been trying to use OpenJML on some popular leaf libraries such org.apache.commons.math3 to check method and specification consistency. I am attaching a toy example where the OpenJML-ESC/Java2 is reporting that method and specification is consistent. However that shouldn't be the case as the method being called here inserts an element into an array. So there should be possible index out of range warnings and so on. Can you please help me understand the possible reason behind this?

davidcok · 2016-11-02T22:05:40Z

Samantha,

Are you using OpenJML or ESC/Java2?2) What version of OpenJML?3) In the GUI, I presume4) What version of Java are you using?5) What OS
You screenshots do not include any specs. What specification did you think is violated?

David

From: Samantha notifications@github.com
To: OpenJML/OpenJML OpenJML@noreply.github.com
Sent: Wednesday, November 2, 2016 5:55 PM
Subject: [OpenJML/OpenJML] Method Specification Inconsistency (Method Specification Inconsistency #481)

Hi All,I have been trying to use OpenJML on some popular leaf libraries such org.apache.commons.math3 to check method and specification consistency. I am attaching a toy example where the OpenJML-ESC/Java2 is reporting that method and specification is consistent. However that shouldn't be the case as the method being called here inserts an element into an array. So there should be possible index out of range warnings and so on. Can you please help me understand the possible reason behind this?
—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub, or mute the thread.

samanthasyeda · 2016-11-03T16:30:33Z

Hi David,

Thank you for your prompt reply.

I am using ESC/Java2 on the program as I need static checking.
I am using the Eclipse plug-in which I downloaded using http://jmlspecs.sourceforge.net/openjml-updatesite, OpenJML version 0.7.3.
Yes, in the GUI
I am using Java 1.7
and OS is Mac OSX Yosemite version 10.10.4.
solver z3_4_3

I was expecting the static checker would give warnings such as Invalid assertion (PossiblyTooLargeIndex). Because the body of the getEntry function called inside getDummyEntry looks like following screenshot.

davidcok · 2016-11-03T17:36:46Z

Samantha,
Thanks for the detail. A note on tools. ESC/Java2 was a previous tool, a precursor to OpenJML, hence my asking to resolve the ambiguity. It will be clearer to say you using 'OpenJML with ESC'; one could also use OpenJML with RAC or for simple type-checking. I'll get back to you on errors in a subsequent message that I don't have time for right now.

David

From: Samantha notifications@github.com
To: OpenJML/OpenJML OpenJML@noreply.github.com
Cc: David Cok cok@frontiernet.net; Comment comment@noreply.github.com
Sent: Thursday, November 3, 2016 12:30 PM
Subject: Re: [OpenJML/OpenJML] Method Specification Inconsistency (Method Specification Inconsistency #481)

Hi David,Thank you for your prompt reply.

I am using ESC/Java2 on the program as I need static checking.
I am using the Eclipse plug-in which I downloaded using http://jmlspecs.sourceforge.net/openjml-updatesite, OpenJML version 0.7.3.
Yes, in the GUI
I am using Java 1.7
and OS is Mac OSX Yosemite version 10.10.4.
solver z3_4_3I was expecting the static checker would give warnings such as Invalid assertion (PossiblyTooLargeIndex). Because the body of the getEntry function called inside getDummyEntry looks like following screenshot.—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub, or mute the thread.

davidcok · 2016-11-03T23:39:10Z

Samantha, The reason that there is no warning on the call of the method fc.getEntry(index) is that there are no specifications for getEntry that limit the range of values that it might have. Checking is done modularly, method by method.So inside getDummyEntry we only check that the implementation of the method, combined with the specifications of any methods it calls, is consistent with the specification of getDummyEntry.
Similarly, getEntry will assessed based on its implementation. However, I don't think you are checking getEntry - I'm guessing that it is a library for which you are using the class files. So its implementation does not get checked. If it were, OpenJML would issue the warning you are expecting.

Try this. Write a ArrayFieldVector.jml file something like
package org.apache.commons.math3.linear;
public class ArrayFieldVector {
    //@ model public int length;
    //@ requires 0 <= index && index < length;
    public void getDummyEntry(int index);
}
Put this file on the classpath, in directory org/apache/commons/math3/linear/
Then try your check again.

David

From: Samantha notifications@github.com
To: OpenJML/OpenJML OpenJML@noreply.github.com
Cc: David Cok cok@frontiernet.net; Comment comment@noreply.github.com
Sent: Thursday, November 3, 2016 12:30 PM
Subject: Re: [OpenJML/OpenJML] Method Specification Inconsistency (Method Specification Inconsistency #481)

Hi David,Thank you for your prompt reply.

I am using ESC/Java2 on the program as I need static checking.
I am using the Eclipse plug-in which I downloaded using http://jmlspecs.sourceforge.net/openjml-updatesite, OpenJML version 0.7.3.
Yes, in the GUI
I am using Java 1.7
and OS is Mac OSX Yosemite version 10.10.4.
solver z3_4_3I was expecting the static checker would give warnings such as Invalid assertion (PossiblyTooLargeIndex). Because the body of the getEntry function called inside getDummyEntry looks like following screenshot.—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub, or mute the thread.

samanthasyeda · 2016-11-04T16:17:21Z

Hi David,

Actually I am interested in the source files of that library itself. I am not using the class file. I have run the OpenJML with ESC tool directly on the ArrayFieldVector class and I get an internal error, although the tool continues to run. I am attaching the snapshot.

Even in this case where I am using the source file, when the tool finishes running I am getting that method and specification are consistent message for the method getEntry(int) that I am interested in. The reason behind using the getDummyEntry() to call one method is I don't want to check specification for all the methods, only one or two methods. Is there any other way of doing so than what I am doing right now? I would like to avoid running the tool on the entire source file e.g. ArrayFieldVector.java.

I understand I am not adding the JML specification, but as I am directly using the source code of the library I was expecting index related warnings from OpenJML with ESC tool and I would like to check whether adding the following gets rid of the warnings.

davidcok · 2016-11-06T09:13:48Z

Samantha, Sorry for the delay in replying. The bug you report is significant and I would appreciate receiving the files you are using so that I can reproduce and fix it. I'll need the files for whichever method produced the internal error and for any classes etc. that are imported by that file.
Thanks, David

  From: Samantha <notifications@github.com>

To: OpenJML/OpenJML OpenJML@noreply.github.com
Cc: David Cok cok@frontiernet.net; Comment comment@noreply.github.com
Sent: Friday, November 4, 2016 12:17 PM
Subject: Re: [OpenJML/OpenJML] Method Specification Inconsistency (#481)

Hi David,Actually I am interested in the source files of that library itself. I am not using the class file. I have run the OpenJML with ESC tool directly on the ArrayFieldVector class and I get an internal error, although the tool continues to run. I am attaching the snapshot.Even in this case where I am using the source file, when the tool finishes running I am getting that method and specification are consistent message for the method getEntry(int) that I am interested in. The reason behind using the getDummyEntry() to call one method is I don't want to check specification for all the methods, only one or two methods. Is there any other way of doing so than what I am doing right now? I would like to avoid running the tool on the entire source file e.g. ArrayFieldVector.java.I understand I am not adding the JML specification, but as I am directly using the source code of the library I was expecting index related warnings from OpenJML with ESC tool and I would like to check whether adding the following gets rid of the warnings.—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub, or mute the thread.

samanthasyeda · 2016-11-07T17:03:17Z

Hi David,

I am attaching the folder to reproduce the error. The main file ArrayFieldVector.java that I am testing is under org.apache.commons.math3.linear package. The other packages contains necessary dependency.

I would like to ask if there is any other way to run the OpenJML tool with ESC on only one method of any class rather than the whole source file?

Thanks in advance!

org.apache.commons.math3.zip

davidcok · 2016-11-07T19:28:08Z

You can run ESC on just one method with the command-line argument -method=... . Put in the name of the method if it is unique or the full package.class.method name. In the GUI, you can select a function name, say in the outline or project explorer view, and right-click to select running ESC.

  From: Samantha <notifications@github.com>

To: OpenJML/OpenJML OpenJML@noreply.github.com
Cc: David Cok cok@frontiernet.net; Comment comment@noreply.github.com
Sent: Monday, November 7, 2016 12:03 PM
Subject: Re: [OpenJML/OpenJML] Method Specification Inconsistency (#481)

Hi David,I am attaching the folder to reproduce the error. The main file ArrayFieldVector.java that I am testing is under org.apache.commons.math3.linear package. The other packages contains necessary dependency.I would like to ask if there is any other way to run the OpenJML tool with ESC on only one method of any class rather than the whole source file?Thanks in advance!org.apache.commons.math3.zip—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub, or mute the thread.

samanthasyeda · 2016-11-07T19:38:32Z

Thanks. However I am getting a duplicate context value error as below:

eclipse.buildId=4.4.2.M20150204-1700
java.version=1.7.0_79
java.vendor=Oracle Corporation
BootLoader constants: OS=macosx, ARCH=x86_64, WS=cocoa, NL=en_US
Framework arguments: -product org.eclipse.epp.package.java.product -keyring /Users/sammy/.eclipse_keyring -showlocation
Command-line arguments: -os macosx -ws cocoa -arch x86_64 -product org.eclipse.epp.package.java.product -keyring /Users/sammy/.eclipse_keyring -showlocation

org.eclipse.core.jobs
Error
Mon Nov 07 13:34:01 CST 2016
An internal error occurred during: "Static Checks - Manual".

java.lang.AssertionError: duplicate context value
at com.sun.tools.javac.util.Context.put(Context.java:138)
at com.sun.tools.javac.util.Context.put(Context.java:194)
at org.jmlspecs.openjml.API.doESC(API.java:794)
at org.jmlspecs.openjml.eclipse.OpenJMLInterface.executeESCCommand(OpenJMLInterface.java:529)
at org.jmlspecs.openjml.eclipse.Utils$2.run(Utils.java:348)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:54)

davidcok · 2016-11-10T12:03:48Z

On a first try I'm missing MathIllegalNumberException and AbstractIntegerDistribution

Which method in particular are you trying to check? Send the command line if you can.

davidcok · 2016-11-10T12:37:11Z

After trying to pull in a few extra files from the apache distribution, I just importe the whole library. Arre you working with a specific version?

samanthasyeda · 2016-11-10T15:34:31Z

I am using the GUI, the method I am interested in is getEntry(int) from org.apache.commons.math3.linear.ArrayFieldVector. I am working with Apache Commons Math 3.6.1 version.

davidcok · 2016-11-12T18:58:33Z

Fixed in V0.8.3, just released. Note that trying to run all of the apache commons library at once will probably run out of memory. But one at a time will probably be OK -- I can successfully run ArrayFieldVector for example.

davidcok · 2016-11-12T19:03:36Z

Let me know if you have any other problems. I'm also interested in what your overall project is.

samanthasyeda · 2016-11-14T23:54:17Z

Hi David,

Thanks for the new version. Unfortunately after updating the new V0.8.3. I couldn't use the tool any more (ESC/JAVA2, OpenJML typecheck etc.). Therefore I deleted the version and reinstalled. Now it is giving me major minor version 52.0 error, I can't even set up preference page for OpenJML.

davidcok · 2016-11-15T03:40:16Z

When you reinstalled, what version did you reinstall?

Try the new version with commandline checking.
Are you sure you are using Java 8?
And I will double check as well.

David

From: Samantha notifications@github.com
To: OpenJML/OpenJML OpenJML@noreply.github.com
Cc: David Cok cok@frontiernet.net; State change state_change@noreply.github.com
Sent: Monday, November 14, 2016 6:54 PM
Subject: Re: [OpenJML/OpenJML] Method Specification Inconsistency (Method Specification Inconsistency #481)

Hi David,Thanks for the new version. Unfortunately after updating the new V0.8.3. I couldn't use the tool any more (ESC/JAVA2, OpenJML typecheck etc.). Therefore I deleted the version and reinstalled. Now it is giving me major minor version 52.0 error, I can't even set up preference page for OpenJML.
—
You are receiving this because you modified the open/close state.
Reply to this email directly, view it on GitHub, or mute the thread.

davidcok · 2016-11-15T04:06:56Z

Samantha -

V0.8.3 is Java 8. Java 8 and Java 7 versions do not play together. I am putting all effort and bug fixes into the Java 8 version.

The major minor version 52.0 error is definitely a sign of mixed versions of Java.
You will need to install Java 8 on your machine, and get the Neon version of Eclipse. I double checked that the eclipse plugin works for me.

David

From: Samantha notifications@github.com
To: OpenJML/OpenJML OpenJML@noreply.github.com
Cc: David Cok cok@frontiernet.net; State change state_change@noreply.github.com
Sent: Monday, November 14, 2016 6:54 PM
Subject: Re: [OpenJML/OpenJML] Method Specification Inconsistency (Method Specification Inconsistency #481)

Hi David,Thanks for the new version. Unfortunately after updating the new V0.8.3. I couldn't use the tool any more (ESC/JAVA2, OpenJML typecheck etc.). Therefore I deleted the version and reinstalled. Now it is giving me major minor version 52.0 error, I can't even set up preference page for OpenJML.
—
You are receiving this because you modified the open/close state.
Reply to this email directly, view it on GitHub, or mute the thread.

samanthasyeda · 2016-11-15T17:24:57Z

Hi David,

My bad! I thought I need to use Java 7.

My overall project is Specification Inference. I am a graduate student at Iowa State University. Currently I am interested in specifications of different libraries.

davidcok · 2016-11-15T18:52:39Z

Samantha,
So as not to clog GitHub up with discussions not related to the bug itself, you are welcome to email me directly (cok@frontiernet.net)I'd like to learn more about your project (are you working with Prof. Rajan?). What actually are you trying to accomplish? Specify all of the apache library? Whatever the project, I'd like to stay in close touch to be sure OpenJML evolves to handle medium and larger scale verification problems.

David

From: Samantha notifications@github.com
To: OpenJML/OpenJML OpenJML@noreply.github.com
Cc: David Cok cok@frontiernet.net; State change state_change@noreply.github.com
Sent: Tuesday, November 15, 2016 12:24 PM
Subject: Re: [OpenJML/OpenJML] Method Specification Inconsistency (Method Specification Inconsistency #481)

Hi David,My bad! I thought I need to use Java 7. My overall project is Specification Inference. I am a graduate student at Iowa State University. Currently I am interested in specifications of different libraries. —
You are receiving this because you modified the open/close state.
Reply to this email directly, view it on GitHub, or mute the thread.

davidcok added a commit that referenced this issue Nov 12, 2016

Fixes to git issue #481

f332c9c

davidcok closed this as completed Nov 12, 2016

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Method Specification Inconsistency #481

Method Specification Inconsistency #481

samanthasyeda commented Nov 2, 2016

davidcok commented Nov 2, 2016

samanthasyeda commented Nov 3, 2016

davidcok commented Nov 3, 2016

davidcok commented Nov 3, 2016

samanthasyeda commented Nov 4, 2016

davidcok commented Nov 6, 2016

samanthasyeda commented Nov 7, 2016

davidcok commented Nov 7, 2016

samanthasyeda commented Nov 7, 2016

davidcok commented Nov 10, 2016

davidcok commented Nov 10, 2016

samanthasyeda commented Nov 10, 2016

davidcok commented Nov 12, 2016

davidcok commented Nov 12, 2016

samanthasyeda commented Nov 14, 2016

davidcok commented Nov 15, 2016

davidcok commented Nov 15, 2016

samanthasyeda commented Nov 15, 2016

davidcok commented Nov 15, 2016

Method Specification Inconsistency #481

Method Specification Inconsistency #481

Comments

samanthasyeda commented Nov 2, 2016

davidcok commented Nov 2, 2016

samanthasyeda commented Nov 3, 2016

davidcok commented Nov 3, 2016

davidcok commented Nov 3, 2016

samanthasyeda commented Nov 4, 2016

davidcok commented Nov 6, 2016

samanthasyeda commented Nov 7, 2016

davidcok commented Nov 7, 2016

samanthasyeda commented Nov 7, 2016

davidcok commented Nov 10, 2016

davidcok commented Nov 10, 2016

samanthasyeda commented Nov 10, 2016

davidcok commented Nov 12, 2016

davidcok commented Nov 12, 2016

samanthasyeda commented Nov 14, 2016

davidcok commented Nov 15, 2016

davidcok commented Nov 15, 2016

samanthasyeda commented Nov 15, 2016

davidcok commented Nov 15, 2016