JML minilab

  1. Save jml4c.jar, jml4rt.jar, and Purse.java into an empty folder.
  2. Read through Purse.java (adapted from figure 1 in Burdy2005), and write down predictions for what will happen when each of the four test methods is executed, in two different cases: (a) when compiling and running using regular Java; (b) when compiling and running using jml4c, a tool that checks JML assertions while a program is running.
  3. Find out whether your predictions were correct. For (a), compile and run Purse.java as usual:
    javac Purse.java
    java Purse.java 1
    java Purse.java 2
    java Purse.java 3
    java Purse.java 4
    
    For (b), compile and run Purse.java using the following commands (on Windows, replace any colon (:) with a semicolon (;)):
    java -jar jml4c.jar -cp "jml4c.jar:." Purse.java
    java -cp "jml4rt.jar:." Purse 1
    java -cp "jml4rt.jar:." Purse 2
    java -cp "jml4rt.jar:." Purse 3
    java -cp "jml4rt.jar:." Purse 4
    
  4. Introduce a deliberate error into the body of one of the methods. You should choose an error that will be detected by the JML spec, and demonstrate this. Be prepared to show this demonstration to the rest of the class.
  5. Fix the previously-introduced error. Now introduce a deliberate error into the JML spec itself. You should choose an error that will be detected by jml4c, and demonstrate this. Be prepared to show this demonstration to the rest of the class.