Witnesses: List appending (out-of-sync)

In this version, the structuring of the definitions leads to many (un)fold annotations. This is because the recursion used for state and list is one step out of sync. In the inline version this is solved by inlining list and in ListAppend it is solved by using a single list predicate.

General information

ID164
Articlenone
Back-endSilicon
LanguageJava
FeaturesLists, Sequences
Sources
Path to example filewitnesses/ListAppendASyncDef.java
Date2017-06-21

Statistical information

Lines of code50 lines (comments not included)
Lines of specification31 lines (62% of the total)
Computation time13797 milliseconds

Example code

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