Dafny互递归类函数decreases子句与Rose树高度函数验证问题

已通过验证的基础定义 #

class RoseTree {
    var NodeType: int
    var id: string
    var children: array<RoseTree>
    ghost var nodeSet: set<RoseTree>

    constructor(nt: int, id: string, children: array<RoseTree>) 
        ensures forall x :: 0 <= x < children.Length ==> children[x].nodeSet <= this.nodeSet
        ensures forall x :: 0 <= x < this.children.Length ==> this.children[x].nodeSet <= this.nodeSet
    {
        this.NodeType := nt;
        this.id := id;
        this.children := children;
        if children.Length == 0 {
            this.nodeSet := {this};
        }else{
            this.nodeSet := {this}+childrenNodeSet(children);
        }
    }
}

function setRosePick(s: set<set<RoseTree>>): set<RoseTree> 
    requires s != {}
{
    var x :| x in s; x
}

function setUnion(setosets: set<set<RoseTree>>) : set<RoseTree> 
    decreases setosets
{
    if setosets == {} then {} else
        var x := setRosePick(setosets);
        assert x <= x + setUnion(setosets-{x});
        x + setUnion(setosets-{x})
}

lemma setUnionDef(s: set<set<RoseTree>>, y: set<RoseTree>)
    requires y in s
    ensures setUnion(s) == y + setUnion(s - {y})
{
    var x := setRosePick(s);
    if y == x {

    }else{
        calc {
            setUnion(s);
            ==
            x + setUnion(s - {x});
            == {setUnionDef(s - {x}, y); }
            x + y + setUnion(s - {x} - {y});
            == { assert s - {x} - {y} == s - {y} - {x}; }
            y + x + setUnion(s - {y} - {x});
            == {setUnionDef(s - {y}, x); }
            y + setUnion(s - {y});

        }
    }
}

lemma setUnionReturns(s: set<set<RoseTree>>) 
   ensures s == {} ==> setUnion(s) == {}
   ensures s != {} ==> forall x :: x in s ==> x <= setUnion(s)
{
    if s == {} {
        assert setUnion(s) == {};
    } else {
        forall x | x in s 
            ensures x <= setUnion(s)
        {
            setUnionDef(s, x);
            assert x <= x + setUnion(s-{x});
        }
    }
}

function childNodeSets(children: array<RoseTree>): set<set<RoseTree>> 
    reads children
    reads set x | 0 <= x < children.Length :: children[x]
{
    set x | 0 <= x < children.Length :: children[x].nodeSet
}

function childNodeSetsPartial(children: array<RoseTree>, index: int): set<set<RoseTree>> 
    requires 0 <= index < children.Length
    reads children
    reads set x | index <= x < children.Length :: children[x]
{
    set x | index <= x < children.Length :: children[x].nodeSet
}

function childrenNodeSet(children: array<RoseTree>): set<RoseTree> 
    reads children
    reads set x | 0 <= x < children.Length :: children[x]
    ensures forall x :: x in childNodeSets(children) ==> x <= childrenNodeSet(children)
    ensures forall i :: 0 <= i < children.Length ==> children[i].nodeSet <= childrenNodeSet(children)
{
    var y := childNodeSets(children);
    setUnionReturns(y);
    setUnion(y)
} 

待验证的height函数实现 #

function height(node: RoseTree):nat 
    reads node
    reads node.children
    reads set x | 0 <= x < node.children.Length :: node.children[x]
    decreases node.nodeSet
{
    if node.children.Length == 0 then 1 else 1 + maxChildHeight(node, node.children,node.children.Length-1,0)
}

function maxChildHeight(node: RoseTree, children: array<RoseTree>, index: nat, best: nat) : nat 
    reads node
    reads node.children
    reads set x | 0 <= x < node.children.Length :: node.children[x]
    requires children == node.children
    requires 0 <= index < children.Length
    ensures forall x :: 0 <= x <= index < children.Length ==> maxChildHeight(node, children, index, best) >= height(children[x])
    decreases node.nodeSet - setUnion(childNodeSetsPartial(children, index)), 1
{
    if index == 0 then best else if height(children[index]) >= best then maxChildHeight(node, children, index-1, height(children[index])) else maxChildHeight(node, children, index-1, best)
}

核心问题 #

• 原证明思路为证明子节点nodeSet是父节点nodeSet的子集、所有子节点nodeSet的并集是父节点nodeSet的子集，以此证明两个互递归函数的终止性，但当前编写的decreases表达式无法通过Dafny验证。
• 已尝试调整childNodeSetsPartial和maxChildHeight为向下递归逻辑，仍未通过验证。
• 附加疑问：类的所有实例是否都会隐式满足构造函数的ensures后置条件，还是仅通过该构造函数显式创建的实例才满足这些条件？

解决方法 #

1. 修正终止度量（decreases）设计 #

原maxChildHeight的递减度量设计过于复杂，且缺少真子集证明，按字典序分层设计度量即可通过验证：

• 对于height(node)，decreases node.nodeSet的设计本身是正确的，但需要补充一个简单引理，证明任意节点不会出现在自己后代的nodeSet中，由此可得任意子节点的nodeSet是父节点nodeSet的真子集（父节点自身在nodeSet中，但不在任何子节点的nodeSet中），满足严格递减要求。
• 对于maxChildHeight，不需要自定义集合差作为度量，直接使用字典序元组decreases node.nodeSet, index即可：
  • 当函数调用height(children[index])时，第一个分量children[index].nodeSet是node.nodeSet的真子集，元组严格递减；
  • 当函数递归调用自身（索引值减1）时，第一个分量node.nodeSet保持不变，第二个分量index严格递减，同样满足字典序的严格递减要求。

替换后Dafny可自动识别递归的终止性，不需要额外的集合差计算逻辑。

2. 构造函数后置条件的生效范围 #

构造函数的ensures后置条件仅对通过该构造函数创建、且创建后未修改相关字段的实例生效。
Dafny不会默认所有类实例都满足构造函数的后置条件：如果类字段是可变的（当前代码中NodeType/id/children/nodeSet都用var定义为可变字段），构造完成后修改字段值就会打破后置条件。如果需要让类的所有实例在任意时刻都满足该性质，有两种方案：

• 用const代替var将相关字段标记为不可变；
• 为类添加invariant不变式，约束所有字段状态始终满足目标性质。

内容的提问来源于stack exchange，提问作者Hath995