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