Verifying Invert Binary Tree

Verifying LeetCode Problem: 266. Invert Binary Tree

Let's take a look at the problem

Given the root of a binary tree, invert the tree, and return its root.

A binary tree is defined by a root node and then between zero and two child nodes branching from it. These child nodes are themselves binary trees. Traditionally the child nodes are labeled the right and left child. What they mean by invert the binary tree is that the left child is swapped with the right child. However, the complication is that they want this done to every node in the tree.

Here is the definition of the data type provided.

 class TreeNode {
     val: number
     left: TreeNode | null
     right: TreeNode | null
     constructor(val?: number, left?: TreeNode | null, right?: TreeNode | null) {
         this.val = (val===undefined ? 0 : val)
         this.left = (left===undefined ? null : left)
         this.right = (right===undefined ? null : right)
     }
 }

An implementation

Here is how we can solve this in JavaScript/TypeScript.

function invertTree(root: TreeNode | null): TreeNode | null {
    if(root == null) return null;
    let leftChild = invertTree(root.left);
    let rightChild = invertTree(root.right);
    root.right = leftChild;
    root.left = rightChild;
    return root;
};

Recursive data structures like a tree are often solved with recursive functions. We start with the base case, where recursion stops. In this case, our function checks if the tree is null and returns null if so. Every branch of a tree will end with null leaves. It recursively inverts all child elements and then swaps the left and right child. This function modifies the tree in place and then returns the modified root.

There is quite a lot going on but lets see the function specification in Dafny to get an idea of what it is that the function does.

method  invertBinaryTree(root: TreeNode?) returns (newRoot: TreeNode?)
    modifies if root != null then root.repr else {}
    requires root != null ==> root.Valid()
    ensures root == null ==> newRoot == null
    ensures root != null ==> newRoot != null && newRoot.repr == old(root.repr) && newRoot.Valid()
    ensures root != null ==> newRoot == root && newRoot.right == old(root.left) && root.left == old(root.right)
    ensures root != null ==> forall node :: node in newRoot.repr ==> node.right == old(node.left) && node.left == old(node.right)
    decreases if root == null then {} else root.repr
{
    if root != null {
        var leftChild := invertBinaryTree(root.left);
        var rightChild := invertBinaryTree(root.right);
        root.right := leftChild;
        root.left := rightChild;
        return root;
    }else{
        return null;
    }
}

The basic problem definition boils down to this line.

ensures root != null ==> newRoot == root && newRoot.right == old(root.left) && root.left == old(root.right)

Dafny has a mechanism, the old() operator which for heap/mutable objects can refer to the value a variable had before it was changed at a certain point in the method. In this case we say the returned root has a left value which is equal to the old right value and likewise the right value is equal to the old left value.

Since this the goal of this method is to invert the entire binary tree we also must make sure that all nodes in the tree are inverted.

ensures root != null ==> forall node :: node in newRoot.repr ==> node.right == old(node.left) && node.left == old(node.right)

Classes in Dafny

To represent mutable data structures in Dafny classes are the preferred method and they have a couple of conventions that are intended to help specifications.

The first is the repr ghost property of a class instance, it represents the set of all objects held by the instance and the instance itself. It is a ghost variable which is not actually part of the compiled code but it is very convenient to use for verification.

ensures root != null ==> newRoot != null && newRoot.repr == old(root.repr) && newRoot.Valid()

If we look at this line of specification it tells us that after the method runs that the tree is still valid and all of the existing nodes are still in the tree and no new nodes were added.

The second is the Valid() method which is a predicate that ensures that each instance is well formed in some way.

class TreeNode {
    var val: int;
    var left: TreeNode?;
    var right: TreeNode?;
    ghost var repr: set<TreeNode>;

    constructor(val: int, left: TreeNode?, right: TreeNode?)
        requires left != null ==> left.Valid()
        requires right != null ==> right.Valid()
        requires left != null && right != null ==> left.repr !! right.repr
        ensures this.val == val
        ensures this.left == left
        ensures this.right == right
        ensures left != null ==> this !in left.repr
        ensures right != null ==> this !in right.repr
        ensures Valid()
    {
        this.val := val;
        this.left := left;
        this.right := right;
        var leftRepr := if left != null then {left}+left.repr else {};
        var rightRepr := if right != null then {right}+right.repr else {};
        this.repr := {this} + leftRepr + rightRepr;
    }

    ghost predicate Valid()
        reads this, repr
        decreases repr
    {
        this in repr &&
        (this.left != null ==>
            (this.left in repr
            && this !in this.left.repr
            && this.left.repr < repr
            && this.left.Valid())
        )
        && (this.right != null ==>
            (this.right in repr
            && this !in this.right.repr
            && this.right.repr < repr
            && this.right.Valid())
        ) && (this.left != null && this.right != null ==> this.left.repr !! this.right.repr && this.repr == {this} + this.left.repr + this.right.repr)
            && (this.left != null && this.right == null ==> this.repr == {this} + this.left.repr)
            && (this.right != null && this.left == null ==> this.repr == {this} + this.right.repr)
            && (this.right == null && this.left == null ==> this.repr == {this})
    }
}

The Valid method is a bit verbose but it is quite powerful and ensures that every tree instance in a valid tree is a contained only within one branch, and it's own subset of nodes, or repr is contained within the parent repr, and all of it's child instances are Valid themselves. It also ensures that no parent node is within the subset of it's child nodes.

This method is important for verification because it ensures that we cover all the relevant cases in our methods. Meaning either a node has no child elements, it has one child either on the left or right, or both children. Then it ensures that our method is not duplicating or reverting work it did earlier because it ensures that every node is only visited once.

Class Method

Although this method was described as a stand alone method, it could also have been implemented as a method of the class.

method  invertBinaryTree() returns (newRoot: TreeNode?)
    modifies this.repr
    requires this.Valid()
    ensures newRoot == this && newRoot.right == old(this.left) && newRoot.left == old(this.right)
    ensures newRoot.repr == old(this.repr) && newRoot.Valid()
    ensures forall node :: node in this.repr ==> node.right == old(node.left) && node.left == old(node.right)
    ensures newRoot.Valid()
    decreases repr
{
    var leftChild: TreeNode? := null;
    if left != null {
        leftChild := left.invertBinaryTree();
    }
    var rightChild: TreeNode? := null;
    if right != null {
        rightChild := right.invertBinaryTree();
    }
    right := leftChild;
    left := rightChild;
    return this;
}