This Website documents the KIV solutions of the VerifyThis Competition held at ETAPS 2021 in Luxembourg, Luxembourg (virtual event). All proofs for challenge 2 were done during the competition, the solutions for challenges 1 and 3 were completed after the event.
KIV-Projects always link to an overview which gives the dependency graph of specifications. Clicking on one specification gives its text, and links to a theorem base summary (which lists names of theorems) and a theorem base listing (which shows the full sequent for each theorem). From there individual theorems and the full details of each proof are accessible.
The Project Overview gives an overview of the entire specification hierarchy of our solution for challenge 1.COMING SOON
We were able to solve all tasks of Challenge 2 during the competition because we could use our library for Separation Logic as seen in the Project Overview.
Here the heap is defined as an algebraic data type over references
r and objects
o with operations for allocation (
h ++ r), deallocation (
h -- r), and reading or updating objects at certain locations (
h[r, o] resp.).
The specification heap-sep defines the common Separation Logic operators like the separating conjunction or the separating implication as higher order predcicates over the heap.
The library also provides a heap-based definition of binary trees using generic nodes with left and right pointers.
We reused these nodes for our definition of doubly-linked lists.
dll(r, x)(h) abstracts the content of a heap
h to an algebraic list
x starting from reference
An auxiliary predicate
dlls(r, r0, r1, x)(h) is used to describe list segments in the heap, the references
r1 point to the nodes to the left and right of the segment.
dlls(r, null, null, x) is equivalent to
Having abstractions of the heap content to algebraic lists and to algebraic trees allows to formulate the required properties using these algebraic data types.
The specification linked-tree-list defines the predicates
balanced(t) that in combination ensure that the algebraic tree
t is a balanced search tree.
An additional function
t.toList calculates a algebraic list for a tree
t that contains the same elements as
t and maintains the order of
The algorithm for the construction of the binary search tree is implemented in the specification DLL2BST with the procedure
The auxiliary procedures
dll_to_bst_rec# are implemented in this specification as well.
Note that we used natural numbers instead of integers in the declarations since negative values are not relevant for the task.
First, we proved the correctness of the
size# procedure with the lemma dll-size-correct which states that if we have a valid doubly-linked list in the heap representing an algebraic list
x, the result in
count is the length
# x of the list.
The proof is by induction over the length of the list and was straightforward, however it was necessary to generalize the lemma by allowing a list segment separated from an arbitrary heap predicate
The main effort was to prove the contract for
We have to ensure that, given a valid list segment
x in the heap, the execution of
dll_to_bst_rec# yields a heap that contains the list segment
x without its first
n elements (
restn(n, x)) and a balanced tree t containing the first n elements of
t.toList = firstn(n, x)).
The contract can be proven by induction over
n, which again requires generalization to a heap with an additional separated heap predicate
After applying the induction hypothesis for both recursive calls it remains mainly to show that both subtrees and the new root node form a combined tree, see goal.
... (right0 => mknode(left0, b, root0) * tr(left0, t) * tr(root0, t0) * ...)(h2) ... ⊦ ∃ t. (tr(right0, t) * ...)(h2) ...This is done with a few interactions by choosing the algebraic tree
mkbranch(t, b, t0)for
tand applying some lemmas from the Separation Logic library. The balanced and same-elements properties for the combined tree are proven automatically using lemmas from linked-tree-list.
Finally, the main proof obligation dll_to_bst_correct can be proven by simply applying the contracts of the two auxiliary procedures:
dll(head, x)(h), ordered≤(x) ⊦ ⦉dll_to_bst#(head; h; root)⦊ ∃ t. tr(root, t)(h) ∧ t.toList = x ∧ ordered≤(t) ∧ balanced(t)Note that we did not have to prove in dll_to_bst_rec_correct that the resulting tree is
ordered≤(t)follows directly from
t.toList = x(see this lemma).
We also solved the additional task and implemented an iterative version of
The correctness proof dll-size-iter-correct could be performed analogously using induction over the length of the list and the correctness of the corresponding main procedure
dll_to_bst_iter# is again proven by using the contracts dll-size-iter-correct and dll_to_bst_rec_correct, see dll_to_bst_iter_correct.
Used basic libraries:
Back to the overview of all KIV projects.
For general informations on KIV and a download site for the whole system refer to this page.
[Imprint] [Data Privacy Statement]