Stack Overflow
Stack Overflow

Questions tagged [jml]

Java Modeling Language (jml) - specification language for Java

The Java Modeling Language (JML) is a behavioral interface specification language that can be used to specify the behavior of Java modules. It combines the design by contract approach of Eiffel and the model-based specification approach of the Larch family of interface specification languages, with some elements of the refinement calculus.

44 questions
9
votes
2 answers

Why isn't JML implemented as Annotations in Java?

Contrary to Code Contracts in C#, in JML Code Contracts are just text that's used in the form of comments in the header of a method. Wouldn't it be better to have them exposed as Annotations, then? That way even when compiling the information would…
devoured elysium
  • 101,373
  • 131
  • 340
  • 557
4
votes
0 answers

JML Error : The .class file appears to be malformed

I am a Teaching Assistant preparing an assignment for my students, in order for them to learn anout JML and design by contract. I give 3 files to them : RArray.refines-java (a specification with blank JML assertions), RArray.java (the class which…
Percelot
  • 41
  • 3
3
votes
1 answer

Simple parser for JML

I am looking for a parser written in Java capable of reading JML. Basically I would like the parser to be able to read a JML block and know to which method it belongs to. I've been looking at the OpenJML project, but just the project setup is too…
Tiago Veloso
  • 8,513
  • 17
  • 64
  • 85
3
votes
2 answers

If statement with return in JML

i need to set up a postcondition which ensures to return null if size_ is 0. Based on if(size_ == 0) return null; how can i do that in jml? any ideas? Following doesn't work: //@ ensures size_ == null ==> \return true; thanks in advance
trnc
  • 20,581
  • 21
  • 60
  • 98
3
votes
1 answer

How do we apply JML (openJML) to Java Code?

How do we apply JML to Java Code? I'm still new in Design by Contracts and quite lost on how to apply it into the program. http://jmlspecs.sourceforge.net/ Using: OpenJML Netbeans 7.3 Java SDK 1.7 I have already added the OpenJML jar files into…
Mark
  • 65
  • 7
3
votes
1 answer

JML postcondition contains class method call

Can a JML postcondition for a class method contain a call to another method call For example I have this class: public class A { public int doA(x) { ... } public int doB(int x, int y) { ... } } For the postcondition of doB can I…
Alina Danila
  • 1,683
  • 1
  • 24
  • 60
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
2
votes
1 answer

JML Alternatives

I am looking for alternative specification languages options for Java, like JML. Does any one know any? Thanks.
Tiago Veloso
  • 8,513
  • 17
  • 64
  • 85
2
votes
1 answer

JML not null variants?

i have a JML questions. what is the difference between /*@ invariant array_ != null; */ and declaring it as protected /*@ non_null */ Object[] array_; regarding the elements of array_? What property holds for them in each case? Thanks in advance.
trnc
  • 20,581
  • 21
  • 60
  • 98
2
votes
1 answer

Programmatic static-checking in OpenJML

The manual for OpenJML (http://jmlspecs.sourceforge.net/OpenJMLUserGuide.pdf) intimates that static-checking of Java compilation units can be done programmatically. Unfortunately, the manual entry for static-checking (Section 5.2.4) is empty, and no…
NietzscheanAI
  • 966
  • 6
  • 16
2
votes
2 answers

Contracts vs Exceptions

Let's assume I have the following code: public class MainClass { public static void main(String[] args) { System.out.println(sumNumbers(10, 10)); } //@requires a >= 10; //@ensures \result < 0; public static int…
devoured elysium
  • 101,373
  • 131
  • 340
  • 557
1
vote
1 answer

JML: \exists & JMLObjectSequence

im trying to prove if there exists a object with a particular status in my collection. My collection consists of objects with a method called getStatus(). Now i want to prove if there is a object with given status in this collection. @ requires…
Bins Ich
  • 1,822
  • 6
  • 33
  • 47
1
vote
1 answer

Cannot prove basic functions relying only on Implementations/Inlining

I have this class Course. I can prove the passed(int i) method when I use the contract for getBar(), not without it. Besides the contract of getBar() is also proven. Why can't I prove passed with inlining? I tried both Key 2.8 and Key 2.7. public…
Dede955
  • 13
  • 2
1
2 3