Witnesses: Magic wand

Demo verification example that shows how magic wands can be used in verification.

General information

ID173
Articlenone
Back-endChalice
LanguageJava
FeaturesLoop invariants, Magic wands, Witnesses
Sources
Path to example filewitnesses/WandDemo.java
Date2017-06-21

Statistical information

Lines of code54 lines (comments not included)
Lines of specification31 lines (57.41% of the total)
Computation time9605 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.