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? ...