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

  • Backend: Silicon
  • Language: Java
  • Features: Sequences, Lists
  • Path to Example File: witnesses/ListAppendASyncDef.java
  • Should Verify: Yes
  • Date: 2017-06-21
  • Lines of Code: 50 (comments not included)
  • Lines of Specification: 31 (62.0% of total)
  • Computation Time: 13.8 seconds