Witnesses: Magic wand (Silver)

Demo verification example that shows how magic wands can be used in verification (with the Silver backend).

General information

ID174
Articlenone
Back-endSilicon
LanguageJava
FeaturesLoop invariants, Magic wands
Sources
Path to example filewitnesses/WandDemoSilver.java
Date2017-06-21

Statistical information

Lines of code51 lines (comments not included)
Lines of specification27 lines (52.94% of the total)
Computation time16126 milliseconds

Example code

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