Common Example

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
  1. Click on commonExample in the Package Explorer (left pane)
  2. Optionally: Select src, default package, and then double-click on ArrayMax.java
  3. 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
  1. Start the KIV system by typing kiv -cosi
  2. Select Projects > Select
  3. Select "normal" and click Okay
  4. Select Exercise 8 and click Okay. You should get a project with a lot of orange specifications (these are libraries) and two blue ovals
  5. 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.