Verify Path Sum

Verifying LeetCode Question: 112. Path Sum

Let's look at the problem definition.

Given the root of a binary tree and an integer targetSum, return true if the tree has a root-to-leaf path such that adding up all the values along the path equals targetSum.

A leaf is a node with no children.

An implementation

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

function hasPathSum(root: TreeNode | null, targetSum: number): boolean {
    if(root == null) {
        return false;
    }
    if(root.val-targetSum == 0 && root.left == null && root.right == null) {
        return true;
    }
    return hasPathSum(root.left, targetSum-root.val) || hasPathSum(root.right, targetSum-root.val);
};

Tree problems are often easily solved with a recursive algorithm.

Breaking this down by cases:
if the current root is null then there is no path which matches the targetSum.

if the current node value matches the targetSum and the current node is a leaf node then we are done, a path exists.

If there is a path in the current nodes left child or if there is a path in the current node right child, minus the current value of this node, then the path exists.

Specifying the implementation

First we define a tree datatype.

datatype TreeNode = Nil | Tree(val: nat, left: TreeNode, right: TreeNode)

We translate the problem definition into two helper functions/predicates. In Dafny, the sequence type, seq is the type of an array like object (i.e it can be indexed into) and it is also like a linked list. assert path == [path[0]+path[1..];

predicate isPath(paths: seq<TreeNode>, root: TreeNode) {
    if |paths| == 0 then false else match paths[0] {
        case Nil => false
        case Tree(val, left, right) => if |paths| == 1 then root == paths[0] else root == paths[0] && (isPath(paths[1..], left) || isPath(paths[1..], right))
    }
}

We say that a path is a sequence of TreeNodes starting from the root. Then if the sequence is not empty and the first node is not Nil and the root is equal to the first node in the list, then if the rest of the list (removing the first element/root) is either a path starting with the roots left child or right child. It will return true or false if is a valid path in the tree.

function pathSum(paths: seq<TreeNode>): nat {
    if |paths| == 0 then 0 else match paths[0] {
        case Nil => 0
        case Tree(val, left, right) => val + pathSum(paths[1..])
    }
}

Given a path, we recursively break the list apart to the first element and the rest of the list, and then add the node value to the pathSum of the rest of the list.

Given these definitions we can translate the problem definition like so:

method hasPathSum(root: TreeNode, targetSum: int) returns (b: bool) 
    ensures b ==> exists p: seq<TreeNode> :: isPath(p, root) && pathSum(p) == targetSum
{
}

Again, we are able to verify the existence of some path p, that sums to the targetSum is the method returns true.

Verifying the implementation

This should be a simple conversion of the TypeScript code to Dafny.

method hasPathSum(root: TreeNode, targetSum: int) returns (b: bool) 
    ensures b ==> exists p: seq<TreeNode> :: isPath(p, root) && pathSum(p) == targetSum
{
    if root == Nil {
        return false;
    }

    if(root.val - targetSum == 0 && root.left == Nil && root.right == Nil) {
        return true;
    }
    var leftPath := hasPathSum(root.left, targetSum-root.val);
    var rightPath := hasPathSum(root.right, targetSum-root.val);

    return leftPath || rightPath;
}

proving the induction to Dafny

Dafny is not immediately convinced of our ensures clause when we write this method. Convincing it is not too difficult but we have to use another Dafny feature.

first resolving the ending case.

if(root.val - targetSum == 0 && root.left == Nil && root.right == Nil) {
  assert isPath([root], root) && pathSum([root]) == targetSum;
  return true;
}

We add an assertion showing that [root] is a valid path and it exists. Secondly if the root value == targetSum then the pathSum([root]) is equal to the targetSum too.

After doing this Dafny will approve of the return condition, but then it will complain about the recursive case.

We call the recursive calls and save the result into a variable, then we break it down into cases.

var leftPath := hasPathSum(root.left, targetSum-root.val);
var rightPath := hasPathSum(root.right, targetSum-root.val);

if leftPath {
  ghost var p: seq<TreeNode> :| isPath(p, root.left) && pathSum(p) == targetSum-root.val;
  assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
}
if rightPath {
  ghost var p: seq<TreeNode> :| isPath(p, root.right) && pathSum(p) == targetSum-root.val;
  assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
}

The new syntax here is a ghost var. A ghost var is a variable that Dafny can use to keep track of data useful to assertions, but it is not actually part of the code that actually runs when a method is run.

It is a variable that only exists in the specification context and not in the execution context of a program.

Secondly, we use the :| operator meaning such that, so basically we can read the following statement like so.

if leftPath {
  ghost var p: seq<TreeNode> :| isPath(p, root.left) && pathSum(p) == targetSum-root.val;
  assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
}

If the leftPath variable is true then inductively hasPathSum says there existed a path p starting at the roots left node and its path sum equals the targetSum-root.val. We assign that path to p. Then we show that if we add the root to that path then that is still a valid path and the pathSum is root.val+(targetSum-root.val) == targetSum. Following the same argument on the right the method verifies.

method hasPathSum(root: TreeNode, targetSum: int) returns (b: bool) 
    ensures b ==> exists p: seq<TreeNode> :: isPath(p, root) && pathSum(p) == targetSum
{
    if root == Nil {
        return false;
    }

    if(root.val - targetSum == 0 && root.left == Nil && root.right == Nil) {
        assert isPath([root], root) && pathSum([root]) == targetSum;
        return true;
    }
    var leftPath := hasPathSum(root.left, targetSum-root.val);
    var rightPath := hasPathSum(root.right, targetSum-root.val);

    if leftPath {
        ghost var p: seq<TreeNode> :| isPath(p, root.left) && pathSum(p) == targetSum-root.val;
        assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
    }
    if rightPath {
        ghost var p: seq<TreeNode> :| isPath(p, root.right) && pathSum(p) == targetSum-root.val;
        assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
    }
    return leftPath || rightPath;
}