prove decreases clause of mutually recursive class functions-CodePudding

I'm having trouble showing how to ensure recursively decreasing functions on a tree class in Dafny. I have the following definitions which verify.

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

In particular I'm trying to define the height function for the tree.

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

I though it should be possible to show that the nodeSet of the node will be a subset of its parent node or that the union of child node sets will be a subset of the parent node, and thus both functions will terminate. My decreases expressions don't prove it to dafny and I'm not quite sure how to proceed. Is there another way to prove termination or can I fix these decrease statements?

Also, do all instances of a class have the constructor ensure statements applied implicitly or only if explicitly constructed using the constructor?

Edit: updated definitions of childNodeSetsPartial and maxChildHeight to recurse downward. It still doesn't verify.

CodePudding user response：

Defining mutable linked heap-allocated data structures in Dafny is not very common except as an exercise. So you should consider whether a datatype would serve you better, as in

datatype RoseTree = Node(children: seq<RoseTree>)

function height(r: RoseTree): int
{
  if r.children == [] then
    1
  else
    var c := set i | 0 <= i < |r.children| :: height(r.children[i]);
    assert height(r.children[0]) in c;
    assert c != {};
    SetMax(c)   1
}

If you insist on mutable linked heap-allocated data structures, then there is a standard idiom for doing that. Please read sections 0 and 1 of these lecture notes and check out the modern version of the example code here.

Applying this idiom to your code, we get the following.

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

    predicate Valid()
      reads this, repr
      decreases repr
    {
      && this in repr
      && children in repr
      && (forall i | 0 <= i < children.Length :: 
            children[i] in repr 
          && children[i].repr <= repr 
          && this !in children[i].repr 
          && children[i].Valid())
    }

    constructor(nt: int, id: string, children: array<RoseTree>) 
      requires forall i | 0 <= i < children.Length :: children[i].Valid()
      ensures Valid()
    {
        this.NodeType := nt;
        this.id := id;
        this.children := children;
        this.repr := {this, children}   
          (set i | 0 <= i < children.Length :: children[i])  
          (set x, i | 0 <= i < children.Length && x in children[i].repr :: x);
    }
}


function SetMax(s: set<int>): int 
  requires s != {}
  ensures forall x | x in s :: SetMax(s) >= x
{
  var x :| x in s;
  if s == {x} then
    x
  else
    var y := SetMax(s - {x});
    assert forall z | z in s :: z == x || (z in (s - {x}) && y >= z);
    if x > y then x else y
}

function height(node: RoseTree): nat
  requires node.Valid()
  reads node.repr
{
  if node.children.Length == 0 then 
    1 
  else 
    var c := set i | 0 <= i < node.children.Length :: height(node.children[i]);
    assert height(node.children[0]) in c;
    assert c != {};
    SetMax(c)   1
}

do all instances of a class have the constructor ensure statements applied implicitly or only if explicitly constructed using the constructor?

I'm not sure if I understand this question. I think the answer is "no", though. Since a class might have multiple constructors with different postconditions.