$ /usr/local/java/jml4c/jml4c.sh Account.java
    /usr/local/java/jml4c/jml4c.sh Account.java
    jml4c.sh called
    CLASSPATH: .:/usr/local/java/jml4c/jml4c.jar:
    bash-3.2$ /usr/local/java/jml4c/jml4.sh Account
    /usr/local/java/jml4c/jml4.sh Account
    jml4.sh called
    CLASSPATH: .:/usr/local/java/jml4c/jml4rt.jar:
    Exception in thread "main" org.jmlspecs.jml4.rac.runtime.JMLInternalPreconditionError:
    By method Account.withdraw
    Regarding specifications at
      File "Account.java", line 27, character 16
    With values
      amt: 200
      bal: 100

        at Account.main(Account.java:36)