This page documents the KIV solutions of the VerifyThis Competition held at ETAPS 2017 in Uppsala, Sweden.
The task of the first challenge was to verify correctness of the Pair Insertion Sort algorithm. For this purpose one had to show that the result of the algorithm is a sorted array and that it is a permutation of the input array. The Project Overview gives an overview over the entire specification hierarchy.
We proved these properties over our abstract nonfree datatype array<oelem> for the given simplified algorithm, transformed into KIV pseudo code (see procedure sort# in the specification pair-insertion-sort). The sortedness property is given by the predicate sorted (specification oarray-sorted) and the permutation property is defined by the predicate perm (specification oarray-perm):
sorted(A, n, m) holds iff the array A is sorted between the indices n (inclusive) and m (exclusive).perm(A, A0) holds iff A and A0 contain the same elements with the same quantity. This is expressed with the algebraic function mkbag(A, n) which calculates the multiset of elements of A up to index n (exclusive).As the algorithm contains multiple (nested) loops, the main difficulty of this challenge was to find suitable invariants for these loops. The program code is extended with the invariants as annotations. There the variable A describes the current state of the array, A` describes the old value of A from just before the first iteration of that particular loop, and the local variable A0 is used to store the value of A at the beginning of the current iteration of the main loop (needed for the inner invariants). We defined an invariant predicate for each loop in the specification sort-invariants.
In each iteration of the main loop the sorted part of array A is extended by two elements. Therefore the first two elements of the unsorted part of A (A[i] and A[i + 1]) are moved forwards inside of A until they are at the right position wrt. sortedness.
Inv-main is that A is sorted up to index i and a permutation of A` (before the loop).The insertion of A[i] and A[i + 1] is done by the two inner loops. The first loop takes the greater element x of the two and shifts all A[j - 1] with x < A[j - 1] ∧ j ≤ i backwards by 2. After that x can be inserted at index j + 1. The second loop continues from the new position of x and iterates further through the array to find the fitting position for the smaller element y and shifts all A[j - 1] with y < A[j - 1] ∧ A[j - 1] ≤ x backwards by 1. To be able to prove that the body of the main loop maintains Inv-main, we need the following invariants for the two inner loops:
Inv-first-inner states that A is sorted from index 0 up to j (exclusive), A is sorted from j + 2 (inclusive) up to i + 2, and that we would have a permutation of A0 if we insert x and y at positions j + 1 resp. j (perm(A[j, y][j + 1, x], A0)).x was inserted after the first inner loop, Inv-last-inner states that A is sorted from 0 up to j and from j + 1 up to i + 2 (note the step from j + 2 to j + 1 compared with Inv-first-inner) . Furthermore A would be a permutation of A0 if we insert y at position j (perm(A[j, y], A0)).The last loop is only executed if the size of the initial array was odd. In this case after executing the main loop we have one element y left that needs to be inserted. Therefore we have to traverse A one last time to find the fitting position for y:
Inv-end for this loop states that the established sortedness of A is maintained and that again A is a permutation of A` as soon as we insert y at index j (perm(A[j, y], A`/)).The actual correctness proof of the algorithm is done via symbolic execution using the defined invariants and some auxiliary theorems about the sorted and perm predicates. We showed total correctness by proving the following goal:
A0 = A ⊦ ⟪sort#(; A)⟫ (sorted(A, 0, # A) ∧ perm(A, A0))
The task of the second (optional) challenge was to verify correctness of Kadane's Algorithm for computing the maximum subarray sum. We proved correctness for the one-dimensional algorithm, i.e., we proved that the result of the algorithm is the sum of a contiguous subarray of the input a and that all possible subarray sums are not greater than the returned value. The Project Overview gives an overview over the entire specification hierarchy.
To express the correctness criterion we first need to define an algebraic sum function over integer-arrays. sum: array<int> × ℕ is defined recursively by:
sum(a, n, 0) = 0
n + m < # a → sum(a, n, m + 1) = sum(a, n, m) + a[n + m]
sum(a, n, m) summates m consecutive values of array a, starting from index n. The precondition n + m < # a of the recursive case ensures that we are only accessing elements within the bounds of a (\# a denotes the length of array a), in other words that we calculate the sum of a valid subarray.
The maximum-sum subarray property is described by the predicate maximum-sum: array<int> × int, which uses the auxiliary predicates maximum-sum: array<int> × ℕ × ℕ × int and upper-bound: array<int> × int:
maximum-sum(a, i) ↔ ∃ n, m. n + m ≤ # a ∧ maximum-sum(a, n, m, i)
maximum-sum(a, n, m, i) ↔ n + m ≤ # a ∧ i = sum(a, n, m) ∧ upper-bound(a, i)
upper-bound(a, i) ↔ ∀ n, m. n + m ≤ # a → sum(a, n, m) ≤ i
Naturally speaking maximum-sum(a, i) holds iff there are some valid n and m such that sum(a, n, m) = i and i is an upper bound for the possible subarray sums of a.
In order to prove this property we need another predicate maximum-suffix-sum: array<int> × ℕ × int that describes the maximum sum i of possible suffix subarrays of a, starting from a valid index n:
maximum-suffix-sum(a, n, i) ↔ n ≤ # a ∧ i = sum(a, n, # a - n) ∧ suffix-upper-bound(a, i)
suffix-upper-bound(a, i) ↔ ∀ n. n ≤ # a → sum(a, n, # a - n) ≤ i
The above operations are defined in the specification int-array-ops.
A KIV pseudo code version of Kadane's Algorithm is implemented in the specification kadane. The correctness proof is done via symbolic execution by proving the following goal:
⟪maxSubArraySum#(a; ; res)⟫ maximum-sum(a, res)
The critical part of the proof is finding a suitable invariant for the loop. The algorithm traverses the input array a sequentially so that after n iterations we can state the following maximum-sum properties for subarray(a, 0, n) (the subarray of a starting at index 0 with n elements, defined in the library specification array-copy):
max_so_far stores the current maximum-sum (maximum-sum(subarray(a, 0, n), max_so_far))
max_ending_here stores the current maximum-suffix-sum starting at some m (∃ m. maximum-suffix-sum(subarray(a, 0, n), m, max_ending_here))
We defined and proved serveral lemmata in int-array-ops to show that the loop maintains these invariants. With these the program proof is straightforward.
Project overview gives an overview over the entire specification hierarchy. The algorithm sorts a list x: list<elem>. The two inner loops swap elements in add and even positions, respectively. And tell the outer loop whether a violation was found by setting issorted to false.
The invariant for the outmost loop is given by
(issorted → ordered≤(x)) ∧ perm(x, x`) ∧ # x = # x`
where x` refers to the variable x in the state before the loop. The predicate ordered≤(x) is defined recursively here and perm(x, y) is defined here by counting the number of occurrences and equating them for all elements.
The termination measure of the outmost loop is
issorted ⊃ 0; (violations(x) + 1)
i.e., if we are already sorted then we are done, otherwise we count the remaining violations in the list. The violations function is defined recursively by
violations([]) = 0
violations(a + x) = less(a, x) + violations(x)
here where less(a, x) counts the number of elements in the list x that are less than a.
The invariant of the first inner loop (where n is odd) is
partial-sorted(x, 1, n) ∧ perm(x, x`) ∧ n ≤ # x ∧ (n % 2 = 1) ∧ # x = # x`
∧ (¬ issorted → violations(x) < violations(x`))
∧ violations(x) ≤ violations(x`)
The predicate partial-sorted(x, offset, m) is defined as
∀ n. offset + 2 * n + 1 < m → ¬ x[offset + 2 * n + 1] < x[offset + 2 * n]
where offset ∈ {0,1}. The predicate expresses that at least the neighboring elements (offset + 2 * n, offset + 2 * n + 1) are correctly ordered. In any case the number of violations does not increase and if we are not yet sorted, then the number of violations actually decreases.
The termination measure for both inner loops is just # x - n, since both loops only iterate over x by increasing the index n (by two).
The invariant of the second inner loop is
(issorted → partial-sorted(x, 1, # x))
∧ partial-sorted(x, 0, n) ∧ perm(x, x`) ∧ n ≤ # x ∧ (n % 2 = 0) ∧ # x = # x`
∧ (¬ issorted` → ¬ issorted)
∧ (issorted` ∧ ¬ issorted → violations(x) < violations(x`))
∧ violations(x) ≤ violations(x`)
and has some additional conjuncts in order the preserve the result of the first loop, at least if we are still sorted.
The program proof can be found here and requires several lemmata about the interaction between swapping elements and the predicates partial-sorted and violations.
Project overview gives an overview over the entire specification hierarchy.
An abstract tree buffer is given by the tree-buffer ASM.
The state is given by the variables h: ℕ and xs: list<elem>.
The ASM provides an implementation for the following interface:
The caterpillar implementation is given by the caterpillar ASM.
It operates on a state h: ℕ, xs: list<elem>, xs_len: ℕ and ys : list<elem>)
The ASM implements the operations of its abstract counterpart.
We have proven the invariants
where # x denotes the length of the list x. The proofs can be seen here and are completely automatic.
The refinement to the abstract specification uses the abtraction relation
prefixn(ah, cxs + cys) = prefixn(ah, axs) ∧ # (cxs + cys) ≤ # axs ∧ ah = ch
where the state variables of the tree buffer specification are prefixed with "a" and those of the implementation with "c".
The proofs can be found here, only the refinement of the operation add# requires the manual application of several lemmas about the prefix function.
The real implementation is given by the implementation ASM.
It has the state
H: ref ⇸ cell, rxs: ref, rys: ref, h: ℕ, xs_len: ℕ, to_delete: list
where
cell = . × .(val: elem, nxt: ref)
is a free datatype for heap cells of a singly-linked list. The heap is given by the explicit partial function H. We have used an algebraic list for the nodes that need to be deleted, instead of a linked-list as in the original version. Note that in to_delete only the head of a list is stored, the list is only incrementally flattened into to_delete.
The abstraction relation is
∃ n. ((ls(crxs, axs) * ls(crys, ays) * del-list(cto_delete, n)))(H) ∧ n ≤ # xs + # ys ∧ n + # xs ≤ h ∧ ch = ah ∧ cxs_len = axs_len
where concrete variables and abstract state variables are again prefixed by "c" and "a", respectively. The predicate ls is the standard list segment predicate of separation logic and the predicate del-list: list<ref> × ℕ is recursively defined by
del-list([], n) = emp ∧ n = 0
del-list(r + rx, n) = ∃ x. ls(r, x) * del-list(rx, n - # x) ∧ r ≠ null ∧ n ≥ # x
The abstraction relation states that the heap can be split into the lists axs and ays starting at their respective references and the nodes that need garbage collection. The additional parameter n stores the number of nodes that need to be deleted. This lets us express the bounds on resources
n ≤ # xs + # ys
as part of the abstraction relation which state that we do not use more than ch - # axs additional resources.
The refinement proofs can be found here. The proof for the operation add# uses a lemma for process_queue#, which states that it removes at most two nodes from the lists referred to by to_delete. The rest of the proof just unfolds the predicate ls appropriately and instantiates its quantifier and the n-quantifier from the abstraction relation. We have also implemented and proved a get# operation.