How do I set up my execution environment for ESC/Java2 in WindowsXP? And furthermore, how do I build and run, in WindowsXP, projects with ESC/Java2. It is hard to tell from their specifications/readme and documentation, specially considering the fact that they seem to be talking more about Unix based operating systems.
...
I would like to know how a JML expression of the form \old(Expression[Id]) is evaluated, i.e. if I have the \old(vector[value-1]) expression, does the \old also refer to "value" or just the to the value of the vector[value-1]. Thanks in advance!
...
I am using Eclipse to program in Java. I tried installing from this site though Eclipse's Updater but although it didn't fire any error, I don't see the menus they say I should.
Maybe I have to install something first? Maybe there other simpler JML options? What you guys use?
...
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 sumNumbers(int a, int b) {
return a+b;
}
}
I can make 2 things here:
Use Code Contr...
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 persist on the .class's metadata, contrary to comments, that get erased.
Am I missing som...
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?
...