tags:

views:

5

answers:

0
Q: 

JML: How to specify a requirement of an array with crescent elements?

I want to do that in JML:

//@ requires (\forall int i : array[i] < array[i+1])
void calculatesDistances(int[] array){
 ..
}

I couldn't make it work, saw a lot of examples in JML specs, but couldn't find a way how to do it.

So, how can i make it?

related questions

Java Time Zone is messed up
Eclipse on win64
Automate builds for Java RCP for deployment with JNLP
Why are professors or schools picking Java over C++ to teach to students?
Is there a real benefit of using J#?
Public/Popular Websites using JavaServer Faces
Why can't I use a try block around my super() call?
Accessing post variables using Java Servlets
Personal Linux web server
Is this really widening vs autoboxing?
How can I Java webstart multiple, dependent, native libraries?
Why can't I call toString() on a Java primitive?
How do I use Java to read from a file that is actively being written?
What code analysis tools do you use for your Java projects?
IllegalArgumentException or NullPointerException for a null parameter?
How do I configure and communicate with a serial port?
What is the best way to parse strings in Java
Getting started with a custom JXTA PeerGroup
Creating a custom button in Java
How to get started "writing" a code coverage tool?
Which Build-/Configuration Management Tool?
What is the difference between an int and an Integer in Java/C#?
What is the meaning of the type safety warning in certain Java generics casts?
How would you access Object properties from within an object method?
Converting CSV File to XML in Java