CSE 102 – Tutorial 9 – Specification, testing, and proof

General instructions

Rigorous specification and proof

In-place list reversal is the process of reversing the order of the elements of a list without creating a new list. In Python, this can be achieved by calling the built-in reverse() method:

In [1]: xs = [0, 1, 2, 3, 4, 5]
In [2]: xs.reverse()
In [3]: xs
Out[3]: [5, 4, 3, 2, 1, 0]

We will consider here two different high-level algorithms for performing in-place list reversal, as well as the corresponding low-level implementations that initially turn out to be incorrect. But before describing the algorithms, we will try to be more precise about what it means for an implementation of in-place list reversal to be correct. That is to say, we will give a rigorous specification of in-place list reversal.

Let us suppose that in-place list reversal is implemented as a function rev taking the input list as argument. For example, rev(xs) could be defined using a call to the built-in reverse() method:

def rev(xs): xs.reverse()

In general, for rev to be a correct implementation of in-place list reversal, then after calling rev(xs) it should be the case that

where xs_input is the original state of the list xs before the call, xs_output is the state of the list after the call, and n is its original length. Here is a Python function that checks this correctness criterion for any given list reversal function revfn on any given input list xs (while leaving the input list unchanged):

def check_rev(revfn, xs):
    n = len(xs)
    xs_copy = xs[:]
    revfn(xs_copy)
    return all (xs_copy[i] == xs[n-1-i] for i in range(n))

An implementation revfn of in-place list reversal is correct just in case check_rev(revfn, xs) evaluates to True for all possible input lists xs. Of course it is not possible to test this automatically, since there are infinitely many lists! So if we want to convince ourselves that an implementation revfn is correct, we have to reason carefully about how it achieves its task. On the other hand, to show that an implementation is incorrect it suffices to find a single counterexample, in the form of a list xs such that check_rev(revfn, xs) evaluates to False.

Now, the first algorithm for in-place list reversal that we consider works by successively swapping elements at opposite ends of the list while moving towards the middle, as illustrated by the following diagram:

Here is a plausible-looking, but buggy, implementation of the algorithm:

def rev1_buggy(xs):
    n = len(xs)
    for k in range(n):
        t = xs[k]
        xs[k] = xs[n-1-k]
        xs[n-1-k] = t

By now you may have noticed the bug that is the reason for the incorrectness of rev1_buggy. (Have you? If not, try to find it before clicking below to reveal a corrected implementation.)

def rev1(xs):
    n = len(xs)
    for k in range(n//2):  # corrected number of loop iterations
        t = xs[k]
        xs[k] = xs[n-1-k]
        xs[n-1-k] = t

You can verify that the corrected in-place list reversal function rev1 deals with your previous counterexample by adding the following line to your Python file and reloading it.

assert check_rev(rev1, xs1)

Of course, this is only a single example, not a proof of correctness on all possible inputs. To convince ourselves that rev1 is a correct implementation of in-place list reversal, we need to try to understand how it goes about reversing a list. For this kind of iterative algorithm, the key is to identify an appropriate “loop invariant”, that is, a condition that is true at the end of each iteration of the for loop, and which implies that the correctness criterion for in-place list reversal holds once all iterations have been completed.

You may have run into this idea before if you are taking CSE103. Here we are not asking you to construct a formal proof in the style of Floyd-Hoare logic, but instead to formulate the loop invariant as a checkable Python condition, and to argue informally that it is always valid and implies the correctness criterion. You should start with the following instrumented version of the corrected implementation:

def rev1_checked(xs):
    xs_input = xs[:]  # we copy the original input list to be able to refer to it in the invariant
    n = len(xs)
    for k in range(n//2):
        t = xs[k]
        xs[k] = xs[n-1-k]
        xs[n-1-k] = t
        assert True   # a formula that should hold at the end of the kth iteration of the loop

An alternative algorithm for reversing the elements of a list works by successively swapping elements to “bubble” up values towards the end of the list, as illustrated by the following diagram:

(This algorithm involves a lot more swapping than the first one, though it only uses swaps of adjacent elements.)

And here is a slightly buggy implementation:

def rev2_buggy(xs):
    n = len(xs)
    for m in range(n,1,-1):
        for i in range(m):
            t = xs[i]
            xs[i] = xs[i+1]
            xs[i+1] = t

Figure out how to fix the bug in rev2_buggy, before clicking below to reveal a corrected implementation.

def rev2(xs):
    n = len(xs)
    for m in range(n,1,-1):
        for i in range(m-1):  # corrected upper bound
            t = xs[i]
            xs[i] = xs[i+1]
            xs[i+1] = t

You will have noticed that the original bug led to check_rev(rev2_buggy, xs2) raising an IndexError exception, rather than returning False. It was implicit in our specification of in-place list reversal that the reversal function should successfully terminate on any input list, without raising an exception or going into an infinite loop. We can improve the check to test explicitly that the function does not raise an exception, as below:

def improved_check_rev(revfn, xs):
    n = len(xs)
    xs_copy = xs[:]
    try:
        revfn(xs_copy)
    except Exception as e:
        return False
    return all (xs_copy[i] == xs[n-1-i] for i in range(n))

(We could also potentially add a timeout to ensure that the call to revfn returns within a reasonable amount of time, although this requires some library support in Python.) Now we can include assertions verifying explicitly that rev2_buggy fails the improved check on the counterexample, and that rev2 passes it.

assert improved_check_rev(rev2_buggy, xs2) == False
assert improved_check_rev(rev2, xs2)

On the other hand, all bets are off if the reversal function is called with something that is not a list. For example, although calling rev2(3.14) raises an exception (TypeError: 'float' object is not subscriptable), this is not considered a specification violation, since the specification states that the input argument should be a list.

def rev2_checked(xs):
    xs_input = xs[:]
    n = len(xs)
    for m in range(n,1,-1):
        for k in range(m-1):
            t = xs[k]
            xs[k] = xs[k+1]
            xs[k+1] = t
            assert True  # inner loop invariant
        assert True  # outer loop invariant

Testing through combinatorial generation

In Tutorial 5 you implemented various operations on binary search trees, including the tricky deletion operation bst_remove which required some careful coding to avoid bugs. Fortunately (or unfortunately!) for you, the submission server’s automated testing was able to frequently identify counterexamples on which your code gave incorrect results. We will now have a retrospective look to see how you could have found these counterexamples on your own.

Let’s begin by recalling the Node class for binary trees, which we’ve augmented with __repr__ and __eq__ methods for the purposes of debugging.

class Node:
    def __init__(self, value, left = None, right = None):
        self.value = value
        self.left = left
        self.right = right
    def __repr__(self):
        return f'Node{(self.value, self.left, self.right)}' if self.left or self.right \
            else f'Node({self.value})'
    def __eq__(self, other):
        return other is not None and \
            self.value == other.value and \
            self.left == other.left and self.right == other.right

Also for the purpose of writing checks, we add a copy method, which returns a fresh copy of a tree.

    def copy(self):
        left  = self.left.copy() if self.left else None
        right = self.right.copy() if self.right else None
        return Node(self.value, left, right)

Your first programming task will be to write a function check_bst_remove that checks whether a given implementation of BST deletion behaves correctly on a given input. But before that, we need to make more precise what exactly defines “correct” behavior.

This requires some thought because there are minor ways that algorithms for BST deletion may differ. For example, the algorithm explained in TD05 makes precise that in the case where the node \(N\) with the value to be deleted has two children you should replace its value by that of its inorder successor — but it would work just as well to take the inorder predecessor. Here are implementations of both approaches:

def bst_remove1(node, x):
    if node is None:
        return None

    if x < node.value:
        node.left = bst_remove1(node.left, x)
    elif x > node.value:
        node.right = bst_remove1(node.right, x)
    else: 
        if node.left is None:
            return node.right
        if node.right is None:
            return node.left
            
        parent, current = node, node.right
        while current.left is not None:
            parent, current = current, current.left
        if parent is node:
            parent.right = current.right
        else:
            parent.left  = current.right
        node.value = current.value
  
    return node 

def bst_remove2(node, x):
    if node is None:
        return None

    if x < node.value:
        node.left = bst_remove2(node.left, x)
    elif x > node.value:
        node.right = bst_remove2(node.right, x)
    else: 
        if node.left is None:
            return node.right
        if node.right is None:
            return node.left
            
        parent, current = node, node.left
        while current.right is not None:
            parent, current = current, current.right
        if parent is node:
            parent.left = current.left
        else:
            parent.right  = current.left
        node.value = current.value
  
    return node

Both of these implementations may be considered as correct, even though they sometimes return different outputs.

An implementation delfn of BST deletion is correct just in case it satisfies the specification for all inputs. Again, since there are infinitely many possible inputs, no amount of testing will guarantee correctness, and the only way to know this for sure is to carefully examine the code and come up with a rigorous explanation for why it works. However, testing can often be used to quickly come up with counterexamples to correctness, which can be a guide in debugging. Two important techniques are exhaustive testing and random testing.

Under exhaustive testing, one generates all possible inputs up to a given size and uses those as test cases. Since the number of possible inputs often grows exponentially as a function of the size, this approach can only be used for testing with relatively small inputs, although it is still useful because often small inputs suffice to find shallow bugs. Under random testing, larger objects are sampled probabilistically and used as test cases. Repeated sampling is then used to try to come up with a counterexample— although again the failure to find one is no guarantee of correctness.

To test implementations of BST deletion, we need to generate pairs of a binary search tree and a value to delete. For simplicity, we will restrict to BSTs with \(n\) nodes labelled by distinct values \(0, \dots, n-1\), and assume that the value to be deleted is an integer between \(0\) and \(n\), and thus either has exactly one occurrence in the tree, or none. (These are pretty safe assumptions, since most reasonable implementations of BST deletion will not depend on the specific values stored in a tree, only making use of relative comparisons. It is possible, though, that some implementations may have bugs in situations where the same value is stored at different nodes of the tree, which would not be caught if we limit ourselves to the space of BSTs with nodes labelled by distinct values.)

Now it’s time to test your testers!

The file buggy.py contains several buggy implementations of BST deletion. By calling testall_bst_remove or testrnd_bst_remove with sufficiently large values, you should be able to find correctness counterexamples for all of them. For example, it is particulary easy to find a counterexample for buggy.del0:

def del0(node, x):
    if node is None:
        return None

In [4]: testall_bst_remove(buggy.del0, 1)
Out[4]: (Node(0), 1)

Verifying an implemention of binary heaps (optional)

Go back and review the definition of binary heaps, as seen in lecture. Here again is the indexing scheme for nodes that can be used to represent binary heaps efficiently as arrays:

def parent(k : int) -> int: return (k-1) >> 1
def left(k : int) -> int:   return (1 + (k << 1))
def right(k : int)-> int:   return (2 + (k << 1))

We limit ourselves to heaps storing string values with associated integer weights, which we represent as lists of string-integer pairs, i.e., values of type list[tuple[str,int]]. The function below checks that such a list satisfies the heap property that the weight of each node is bounded from above by the weights of each of its children, or equivalently, bounded from below by the weight of its parent.

def is_heap(heap : list[tuple[str,int]]) -> bool:
    for i in range(1,len(heap)):
        if heap[i][1] < heap[parent(i)][1]:
            return False
    return True

Our overall goal is to correctly implement the insertion (heappush) and removal (heappop) operations,

def heappush(H : list[tuple[str,int]], a : str, w : int) -> None:
    pass
    
def heappop(H : list[tuple[str,int]]) -> tuple[str,int]:
    pass

as explained during the lecture and illustrated below.

heappush:

heappop:

13. Using the testing routines described during class to help you with debugging, implement heappush and heappop. For convenience we copy all of the testing code below, which you are free to modify.

    class InvalidHeap(Exception):
        def __init__(self, H):
            self.H = H
    
    def heap_sort(xs : list[int]) -> list[int]:
        """sorts a list of integers using a binary heap"""
        H : list[tuple[str,int]] = []
        for i in range(len(xs)):
            heappush(H, str(i), xs[i])
            if not is_heap(H): raise InvalidHeap(H)
        output = []
        while H:
            output.append(heappop(H)[1])
            if not is_heap(H): raise InvalidHeap(H)
        return output
    
    def is_sorted(l):
        """returns True if the input list is sorted, and False otherwise."""
        for i in range(len(l)-1):
            if l[i+1] < l[i]:
                return False
        return True
    
    def randperm(n):
        """returns a permutation of 1..n chosen uniformly at random"""
        if n == 0: return []
        else:
            p = randperm(n-1)
            i = random.randrange(n)
            return p[:i] + [n] + p[i:]
    
    def test_heapsort(n, k=10000):
        """tests correctness of heappush and heappop by calling heap_sort on random permutations"""
        for _ in range(k):
            xs = randperm(n)
            assert is_sorted(heap_sort(xs))

14. (Hard!) Once you are sufficiently convinced that your implementation of heappush and heappop is correct, prove it by writing down a rigorous specification of both functions and identifying the necessary loop invariants. (You can also start directly from the implementations shown in the last two slides of Lecture 10, but writing and debugging your own code is a good exercise, and there is definitely room for more efficient implementations.)