Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
bank_account_example_in_jahob [2007/05/14 12:33] vkuncak |
bank_account_example_in_jahob [2007/05/14 12:36] vkuncak |
||
|---|---|---|---|
| Line 4: | Line 4: | ||
| You can also download the example: {{Account.java.txt}} | You can also download the example: {{Account.java.txt}} | ||
| + | |||
| + | The command to verify this example is | ||
| + | ../../bin/jahob.opt Account.java -class Account -sastvc -usedp cvcl | ||
| + | and requires an SMT-LIB solver under the name 'cvcl' to be installed to work (download[[http://www.cs.nyu.edu/acsys/cvc3/|CVC3]] and create a symlink to that executable). | ||
| <code java> | <code java> | ||