binary-tree - Dafny 中的二叉树

Question

来自办公室的问题 - 树的边界是从左到右顺序的提示值序列。我需要开发迭代代码，使用以下 IO 类的 OUTPUT 方法打印给定树的边界

class IO<T> {
    var alpha: seq<T>, omega: seq<T>;

    method Input() returns (x: T)
        requires !EOF() //alpha != []
        modifies this
        ensures omega == old(omega)
        ensures old(alpha) == [x] + alpha
    {
        x, alpha := alpha[0], alpha[1..];
    }

    method Output(x: T)
        modifies this
        ensures alpha == old(alpha)
        ensures omega == old(omega) + [x]
    {
        omega := omega + [x];
    }

    method Rewrite()
        modifies this
        ensures omega == []
        ensures alpha == old(alpha)
    {
        omega := [];
    }

    predicate method EOF() reads this { alpha == [] }

}

method Main()
{
    var tree: BT<int>;
    tree := Tip(1);
    var io: IO<int>;
    io := new IO<int>;
    FrontierIter(tree, io);
    print io.omega;

    io.Rewrite();
    tree := Node(tree, Tip(2));
    FrontierIter(tree, io);
    print io.omega;
}

function Frontier(tree: BT<T>): seq<T>
{
    match tree {
        case Tip(n) => [n]
        case Node(left, right) => Frontier(left) + Frontier(right)
    }
}

method FrontierIter(tree: BT<T>, io: IO<T>)
    requires io != null
    modifies io
    ensures io.omega == old(io.omega) + Frontier(tree)
{
    var stack: seq<BT<T>>;
    stack := [tree];