COST Verification Competition : KIV Solutions

More information on the competition can be found here: http://foveoos2011.cost-ic0701.org/verification-competition

General comments

Challenge 1 : Maximum of an array

Given: A non-empty integer array a.
Verify that the index returned by the method max() given below points to an element maximal in the array.

public class Max {

    public static int max(int[] a) {
        int x = 0;
        int y = a.length-1;

        while (x != y) {
            if (a[x] <= a[y]) x++;
            else y--;
        }
        return x;
    }
}

Solution A slightly optimized solution which defines a simpler max-function can be found here. A further solution uses KIV's Java calculus to verify a Java implementation of the challenge here.

Challenge 2: Maximum in a tree

Given: A non-empty binary tree, where every node carries an integer. Implement and verify a program that computes the maximum of the values in the tree. Please base your program on the following data structure signature:

public class Tree {

    int value;
    Tree left;
    Tree right;

}
You may represent empty trees as null references or as you consider appropriate.

Solution

Basically this refines an algebraic maximum function defined on freely generated trees to a maximum procedure computing on pointer based trees, using lightweight separation logic to establish disjunctness.

Challenge 3: Two equal elements

Given: An integer array a of length n+2 with n>=2. It is known that at least two values stored in the array appear twice (i.e., there are at least two duplets).
Implement and verify a program finding such two values.
You may assume that the array contains values between 0 and n-1.

Solution

Challenge 4: Cyclic list

Given: A Java linked data structure with the signature:

public class Node {

    Node next;
    
    public boolean cyclic() {
        //...
    }

}
Implement and verify the method cyclic() to return true when the data structure is cyclic (i.e., this Node can be reached by following next links) and false when it is not.

Solution

Specification challenge4 contains the two algorithms of Floyd and Brent, both modified to check for null-pointers from the wikipedia page.

The two main proofs are challenge4-Floyd and challenge4-Brent. Both proofs are rather tricky.

They first distinguish between cyclic and acyclic structures, since the two cases need different variants for termination.

The noncyclic case induces over the difference of the length of the list minus the number of steps done for the faster pointer (the "hare"). For Floyd this needs wellfounded induction since it decreases by two on every iteration.

The cyclic case needs the characterizations cyclic-floyd-def and cyclic-brent-def (two theorems) from specification cyclic, to get the variant right.

cyclic-floyd-def gives an r0 such that r0 is reachable from r as well as from r0 in n steps. Termination is then, since n minus the steps of the slower pointer (the "tortoise") decreases.

cyclic-brent-def gives an r0 that is reachable in 2^n - 1 steps, such that from r0 a cycle with m ≤ 2^n steps starts. Termination is then, since 2^n -1 + m minus the steps of the faster pointer decreases by one in each loop iteration.

Since the variants of both proofs require existentially quantified variables from the invariant, the proof does not work by simply applying the invariant rule. Instead we generalize the precondition to the invariant with the cut formula rule (blue color). This gives two goals: one that proves precondition → invariant, in the other we get both precondition and invariant, and weaken (brown color) the initial values of the variables modified in the loop. The existential quantifier gets dropped by simplification. Then we use induction over the size of the variant (red color).

The proof proceeds by exiting the loop in the base case. For the recursive case, the loop is unwound once (violet colour), then the induction hypothesis is applied (green color for the three structural inductions, red color for the one wellfounded induction).

In specification cyclic, theorems cyclic-floyd-def and cyclic-brent-def are two of 6 characterizations of cyclicity, that are all proven to be equivalent. The other four are:

  1. The original axiom cyclic-def defines cyclic(r), iff an r0 is reachable from r in both m and n steps, where m < n.
  2. Theorem cyclic-alt-def says, that cyclic(r) iff some r0 is reachable from r, such that r0 is reachable from itself in n * n0 steps for all n0 (n is the length of the cycle), so it is slighly stronger that the original axiom.
  3. Theorem cyclic-weak-def says this is equivalent to that for all lengths n an element is reachable from r (the equivalence proof is based on finiteness of the heap).
  4. Finally, theorem legal-noncylic-equiv-reaches-null says that for a heap H without dangling pointers (predicate legal in specification cyclic), r is acyclic iff it reaches the null pointer in finitely many steps.

Theorems that are often used are:



[Impressum] [E-Mail]