Witnesses: List iterator

Verifying a list iterator, implemented in Java, using witness encodings. Note that depending on which version of chalice is used, this spec may take a very very long time to check. Also, this example currently does not verify because it must be rewritten.

General information

ID166
Articlenone
Back-endChalice
LanguageJava
FeaturesLists, Loop invariants, Magic wands, Witnesses
Sources
Path to example filewitnesses/ListIterator.java
Date2017-06-21

Statistical information

Lines of code263 lines (comments not included)
Lines of specification162 lines (61.6% of the total)
Computation timeunknown

Example code

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