[CS 378] Runtime monitoring checking

[David L. Rager]

Hello Students,

You can see the below for an example of how to do java runtime monitoring using
JML notations. If you have questions, *please ask on the newsgroup*.

David

---- Example.java ----

public class Example {

public int i = 0;

//@ invariant (i == 0 || i!= 0);
public void increment() {
i++;
}

public static void main(String[] args) {
Example ex = new Example();
ex.increment();

}

}

---- End Example.java ----

---- From a UTCS prompt in a directory with Example.java saved -----

/v/filer4b/v23q001/apetrov/jml/bin/jmlc Example.java
/v/filer4b/v23q001/apetrov/jml/bin/jmlrac Example