Dafny exists expression can't deal with references?

Question

I'm trying to define an operation on classes and then prove properties about it.

    //the following resolves the error with substring, but creates problems down the line
    //predicate isSubstring<A(!new)>(sub: seq<A>, super: seq<A>) {
    predicate isSubstring<A>(sub: seq<A>, super: seq<A>) {
        |sub| <= |super| && exists xs: seq<A> :: IsSuffix(xs, super) && sub <= xs
    }

    predicate IsSuffix<T>(xs: seq<T>, ys: seq<T>) {
        |xs| <= |ys| && xs == ys[|ys| - |xs|..]
    }

However, the IsSubstring method produces the following error.

a exists expression involved in a predicate definition is not allowed to depend on the set of allocated references, but values of 'xs' may contain references (see documentation for 'older' parameters

I am aware that I can set (!new) restriction on the type variable A. That resolves the issue at the predicate. However I am presented with another issue.

lemma AllChildrenTraversalsAreSubstrings(root: TreeNode) 
    requires root.Valid()
    ensures forall x :: x in root.repr && x in PreorderTraversal(root) ==> isSubstring(PreorderTraversal(x), PreorderTraversal(root))
{
    forall x | x in root.repr && x in PreorderTraversal(root) 
        ensures isSubstring(PreorderTraversal(x), PreorderTraversal(root))
    {
        if x == root {

        }else if x == root.left || x == root.right {
           PreorderTraversalSubstrings(root); 
        }else {
            if root.left != null && x in root.left.repr {
                AllChildrenTraversalsAreSubstrings(root.left);
            }
            if root.right != null && x in root.right.repr {
                AllChildrenTraversalsAreSubstrings(root.right);
            }
        }
    }
}

In the forall ensure it reports:

type parameter (A) passed to predicate isSubstring must support no references (got TreeNode)

function method PreorderTraversal(root: TreeNode): seq<TreeNode>
    reads root.repr
    requires root.Valid()
    // ensures forall x :: x in PreorderTraversal(root) ==> x.Valid()
    ensures forall x :: x in root.repr ==> x in PreorderTraversal(root)
    ensures forall k :: 0 <= k < |PreorderTraversal(root)| ==> PreorderTraversal(root)[k] in root.repr && PreorderTraversal(root)[k].Valid()
    ensures injectiveSeq(PreorderTraversal(root))
    ensures forall k :: 0 <= k < |PreorderTraversal(root)| ==> PreorderTraversal(root)[k] in root.repr
    // ensures forall k :: 0 <= k < |PreorderTraversal(root)| ==> forall child :: child in PreorderTraversal(root)[k].repr && child != child in PreorderTraversal(root)[k] ==> exists j :: k < j < |PreorderTraversal(root)| && PreorderTraversal(root)[j] == child
{
   if root.left != null && root.right != null then [root]+PreorderTraversal(root.left)+PreorderTraversal(root.right) else if root.left != null then [root]+PreorderTraversal(root.left) else if root.right != null then [root]+PreorderTraversal(root.right) else [root]
}

lemma PreorderTraversalSubstrings(root: TreeNode)
    requires root.Valid()
    ensures root.left != null ==> isSubstring(PreorderTraversal(root.left), PreorderTraversal(root))
    ensures root.right != null ==> isSubstring(PreorderTraversal(root.right), PreorderTraversal(root))
{
   if root.left != null && root.right != null {
    calc {
        PreorderTraversal(root);
        [root]+PreorderTraversal(root.left)+PreorderTraversal(root.right);
    }
    assert |PreorderTraversal(root.left)| < |PreorderTraversal(root)|;
    assert |PreorderTraversal(root.right)| < |PreorderTraversal(root)|;
    assert IsSuffix(PreorderTraversal(root.left)+PreorderTraversal(root.right), PreorderTraversal(root));
    assert IsSuffix(PreorderTraversal(root.right), PreorderTraversal(root));
    assert PreorderTraversal(root.left) <= PreorderTraversal(root.left)+PreorderTraversal(root.right);
   }else if root.left != null && root.right == null {
    calc {
        PreorderTraversal(root);
        [root]+PreorderTraversal(root.left);
    }
    assert |PreorderTraversal(root.left)| < |PreorderTraversal(root)|;
    assert IsSuffix(PreorderTraversal(root.left), PreorderTraversal(root));
   }else if root.left == null && root.right != null {
    calc {
        PreorderTraversal(root);
        [root]+PreorderTraversal(root.right);
    }
    assert |PreorderTraversal(root.right)| < |PreorderTraversal(root)|;
    assert IsSuffix(PreorderTraversal(root.right), PreorderTraversal(root));
   }
}

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;
    }

    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})
    }
}

Oddly enough,PreorderTraversalSubstrings verifies just fine even with the (!new) restriction but the ensure statement of the forall in AllChildrenTraversalsAreSubstrings throws the above error. How should I proceed? Switching to a datatype would make my life easier but I'm trying to verify programs involving classes.

Do I define the binary tree datatype and then assert that all operations on it are equivalent to the valid class tree version? Is that even possible if existence quantifier expressions can't refer to allocated value?

Answer 1

The solution to the problem you run into with your definition of isSubstring is not that you should use the type characteristic !new but rather that you should not use existential quantification in your definition. In the end, I presume that you mean for isSubtring to be a predicate method that can be compiled and executed, so it cannot be defined in terms of an existential quantifier.