Currently, we provide one common example: finding the maximum in an array. The example is currently available for the following tools:
| Tool | Browse code | Load/run example in the tool
(execute in corresponding subdir of commonExample) | Comments | | Boogie | ArrayMax in Boogie | Boogie.exe ArrayMax.bpl | | | Dafny | ArrayMax in Dafny | Dafny.exe ArrayMax.dfy | | | ESC/Java | ArrayMax in ESC/Java | eclipse | - Click on commonExample in the Package Explorer (left pane)
- Optionally: Select src, default package, and then double-click on ArrayMax.java
- Use the ESC/Java2 menu at the top
| | Jahob | ArrayMax in Jahob | jahob.opt ArrayMax.java B.java | | | KeY | ArrayMax in KeY | runProver ArrayMax.java | Select the max() method in the load dialog, then the ensuresPost proof obligation and the default contract. Click the green play button. | | KIV | ArrayMax in KIV | kiv -cosi | - Start the KIV system by typing
kiv -cosi - Select Projects > Select
- Select "normal" and click Okay
- Select Exercise 8 and click Okay. You should get a project with a lot of orange specifications (these are libraries) and two blue ovals
- Left-click on the blue oval named ArrayMax, select "Work on..." from the menu and click Okay
See doc/KIV-documentation.pdf (Chapter 14) for details. | | Krakatoa | ArrayMax in Krakatoa | gwhy ArrayMax.java | Click the SMT solver (e.g., alt-ergo) column headers. | | VeriFast | ArrayMax in VeriFast | vfide ArrayMax.java | From the Verify menu select "Verify program". Uncheck "Check arithmetic overflow" in the same menu. |
| 