Stack Overflow
Stack Overflow

Questions tagged [openjml]

OpenJML is a tool for working with logical annotations in Java programs.

OpenJML is a tool for working with logical annotations in Java programs. It enables static or run-time checking of the validity of the annotations; it also provides an enhanced version of javadoc that includes the annotations in the javadoc documentation.

14 questions
21
votes
2 answers

Reasoning about reals

I am experimenting with OpenJML in combination with Z3, and I'm trying to reason about double or float values: class Test { //@ requires b > 0; void a(double b) { } void b() { a(2.4); } } I have already found out OpenJML uses AUFLIA…
nhaarman
  • 98,571
  • 55
  • 246
  • 278
4
votes
1 answer

Contract Checking in Maven Build

I'm working on a Java codebase in IJ and currently building with Maven. I would like to supplement some of the code with some form of contracts that will get picked up in the Maven build. So far, I've been unsuccessful in my search for such a…
Colm Bhandal
  • 3,343
  • 2
  • 18
  • 29
2
votes
0 answers

OpenJML warning in Java

I am new to JML warnings and I am trying to remove all warnings for this function: //@ requires input <= Integer.MAX_VALUE; //@ requires input >= 0; //@ ensures \result >= 0; //@ signals (Exception) input >= Integer.MAX_VALUE; //@ ensures result ==…
user122222
  • 2,179
  • 4
  • 35
  • 78
2
votes
1 answer

JML remove warning after calling a function

I'm given a task where I have to remove every warning produced by JML. If I call a method inside the constructor my requires and ensures are not verified anymore, despite adding the same constraint for the called function. I am asked to use only…
LucaBonadia
  • 91
  • 2
  • 12
2
votes
1 answer

How to remove spaces after comments in Eclipse auto formatting?

I'm using the OpenJML plugin for my project, but Eclipse auto formatting messes with my JML code. JML is written after a //@ symbol. //@ requires password != null; //@ ensures !isActive() && getPassword().testWord(password) ? isActive() && \result :…
HYBR1D
  • 464
  • 2
  • 6
  • 19
1
vote
1 answer

Why OpenJML can not prove an assertion in for cycle?

I have the following piece of code: //@ requires dest != null; //@ requires srcOff >= 0; //@ requires destOff >= 0; //@ requires length >= 0; //@ requires srcOff < src.length; //@ requires destOff < dest.length; //@ requires srcOff + length <=…
Francesco
  • 897
  • 8
  • 22
1
vote
1 answer

OpenJML/Jessie for android

I am trying to statically check Java my code. The only problem is that it uses android sdk and OpenJML cannot identify android classes. For instance this is part of logs I get: app/src/main/java/rup/ino/catornot/MainActivity.java:3: error: package…
alagris
  • 1,838
  • 16
  • 31
0
votes
0 answers

JML typing error: a memory state is needed here (\at missing?)

I've been trying to fix an error in my JML program, but I haven't been able to do it. It's a typing error that references to a file, "Practi.jc" that I have no clue about where it is neither. //@+CheckArithOverflow=no /*@ axiomatic Addition{ @logic…
Nuria
  • 1
  • 1
0
votes
1 answer

Correct way to install JML

I tried to install Java modeling language (JML) and something got wrong. I use Eclipse IDE, windows 10. I opened Eclipse -> Help -> Install New Software and then I installed using this Then, I restarted Eclipse and the new icons appeared in the top…
dacian
  • 95
  • 1
  • 8
0
votes
1 answer

Key Java JML proover passes this algorithm that reads a specific array element which triggers a NullPointerException? it should fail instead

I'm tyring to better understand the limits of the Key proover for Java. I have come up with a scenario where a specific array element will trigger a null pointer exception. When I run this through the proover it passes. Any idea why this is? It…
newlogic
  • 807
  • 8
  • 25
0
votes
1 answer

JML - OpenJML with Extended Static Checking - Array Example

I just started to use OpenJML, here my code and my JML warning: Code : //@ requires myArray != null ; //@ ensures myArray == \old(myArray) ; //@ signals ( MathLibException ) myArray.size() == 1 ; public ArrayList ExceptionTest1…
Gabriel
  • 1
  • 1
0
votes
1 answer

How can I see the OpenJML error messages?

When I run my code with the OpenJML test in eclipse. I get this output ...... Skipping long-running tests 5 system specification classes found for esc testing JRE version 1.8.0_202 5 system specification classes found for rac testing TEST:…
Siri Framboise
  • 1
  • 1
0
votes
1 answer

Use OpenJML in Eclipse project that uses JDK different from OpenJDK 1.8

OpenJML is available as Eclipse Plugin (install site http://jmlspecs.sourceforge.net/openjml-updatesite ) and it seems to get installed OK in Eclipse Photon. But docs say it shall run only on OpenJDK 1.8 and it cannot be any other JDK (say, Oracle…
Code Complete
  • 3,146
  • 1
  • 15
  • 38
0
votes
1 answer

Iterate through a matrix with openJML

I have a class with a matrix initialized with all 0 and 1 in a specific position: public class MatrixTest { /*@ spec_public @*/ int[][] griglia; //@requires true; //@ensures griglia[2][3] == 1; public MatrixTest() { griglia…
gbalduzzi
  • 9,356
  • 28
  • 58