Witnesses: List appending (magic wand)

This example shows how to use the _given_ keyword to pass verification level arguments and also how to use a magic wand to prove the iterative implementation of list append correct.

General information

ID163
Articlenone
Back-endSilicon
LanguageJava
FeaturesLists, Magic wands, Sequences, Witnesses
Sources
Path to example filewitnesses/ListAppend.java
Date2017-06-21

Statistical information

Lines of code108 lines (comments not included)
Lines of specification62 lines (57.41% of the total)
Computation time25570 milliseconds

Example code

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