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.
|Features||Lists, Magic wands, Sequences, Witnesses|
|Path to example file||witnesses/ListAppend.java|
|Lines of code||108 lines (comments not included)|
|Lines of specification||62 lines (57.41% of the total)|
|Computation time||25570 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.