我無法展示如何確保在 Dafny 的樹類上遞回遞減函式。我有以下定義可以驗證。
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)
}
特別是我試圖為樹定義高度函式。
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 將是其父節點的子集，或者子節點集的并集將是父節點的子集，因此這兩個函式都將終止。我減少的表達并不能證明它對 dafny 來說，我不太確定如何繼續。是否有另一種方法來證明終止或者我可以修復這些減少陳述句？
此外，一個類的所有實體是否都隱式應用了建構式確保陳述句，或者僅在使用建構式顯式構造時應用？
編輯：更新了 childNodeSetsPartial 和 maxChildHeight 的定義以向下遞回。它仍然沒有驗證。
uj5u.com熱心網友回復：
在 Dafny 中定義可變鏈接堆分配資料結構并不常見，除非作為練習。因此，您應該考慮資料型別是否會更好地為您服務，例如
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
}
如果您堅持使用可變鏈接堆分配的資料結構，那么有一個標準的習慣用法。請閱讀這些講義的第 0 部分和第 1 部分，并在此處查看示例代碼的現代版本。
將此習語應用于您的代碼，我們得到以下內容。
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
}
一個類的所有實體是否都隱式應用了建構式確保陳述句，或者僅在使用建構式顯式構造時應用？
我不確定我是否理解這個問題。不過，我認為答案是“不”。因為一個類可能有多個具有不同后置條件的建構式。
轉載請註明出處，本文鏈接：https://www.uj5u.com/gongcheng/487726.html