Aは不変であるが、このコードで

Question

https://rise4fun.com/Dafny/DmBh

アサートFORALL X :: X multisetOfTree（t.right）で==> t.root < = Xを証明することはできません。

は36行目では証明されていませんが、それは不変式の一部です。 実際には、31行目の不変量をコメント解除し、36行目と のコメントを付けることができます。

Answer 1

isABBの定義に括弧がないことが問題です。

読み込みする必要があります。

predicate isABB (t:Tree<int>) 
{ 
match t 
    case Empty => true 
    case Node(l,d,r) => isABB(l) && isABB(r) 
         && (forall x :: x in multisetOfTree(l) ==> x <= t.root) 
         && (forall x :: x in multisetOfTree(r) ==> t.root <= x) 
}