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.
Challenge 1 (Challenge 1 - Lexicographic Permutations ⤓ (PDF)) provided a code snippet to be verified for generating all permutations of the elements of a array. It should be shown that the permutations are created completely and in lexicographic order (besides properties like termination and bounds checking). For this, we defined a lexicographic ordering on such arrays in our main specification challenge1. These are based on the oarray-sort specification from our library, so on the one hand we could fall back on predicates for sorted arrays as well as a predicate "perm" from specifiaction list-perm, which states whether 2 lists are permutations of each other. This was possible because the used arrays were based upon a list definition as seen in the Project Overview. Furthermore, we specified for permutations what it means to be a "next" permutation in the lexical order and to be the "last", i.e. maximal one. Thus, corresponding postconditions for the routine next# could be formulated. To show completeness, we introduced a predicate "min" describing what is a smallest permutation with respect to the lexicographic order.
The main proof obligation is permut-correct for routine permut# and next-proper-permutation for next#. All loop invariants and terms for termination are placed into the code of the routines.
A challenge for proofing next# was to show that the resulting array is indeed a next permutation. An important lemma is that the problem whether the output is the next permutation to the input can be reduced to the longest different suffix, i.e. a common prefix can be neglected. Finally, 3 main cases are distinguished, how a possible permutation P could look like, so that it would be between the suffix of input and output (in the following referred to as I and O):
The task definition can be downloaded from ETH Zürich: Challenge 2 - DLL to BST ⤓ (PDF)
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.
A description of the callenge can be found at: Challenge 3 - ShearSort ⤓ (PDF) (external link to ETH Zürich)A sequential version of this challenge (with an optimization) was solved offline. (Update: an extension to a concurrent version is now available too). To find a solution two steps are crucial: First it is necessary to find out, how the 0-1-Principle must be applied to an algorithm. This is done by fixing an arbitrary element i and marking all elements as 0/1 that are less/greater or equal than i. Second the crucial argument, why one row- and then column sort halves the number of dirty rows must be understood and then formalized. Our formalization (see this link for an overview) uses the following main specifications and predicates:
|[Hagerup16]|| T. Hagerup
Course notes: Introduction to Parallel Algorithms
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]