Witnesses: Magic wand (Silver)
Demo verification example that shows how magic wands can be used in verification (with the Silver backend).
|Features||Loop invariants, Magic wands|
|Path to example file||witnesses/WandDemoSilver.java|
|Lines of code||51 lines (comments not included)|
|Lines of specification||27 lines (52.94% of the total)|
|Computation time||16126 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.