A forall das ist unveränderlich, aber nicht

Question

In diesem Code

https://rise4fun.com/Dafny/DmBh

assert forall x :: x in multisetOfTree (s.rechts) ==> t.root < = x bewiesen werden;

ist nicht in Zeile 36 bewiesen, aber es ist Teil der Invariante. In der Tat können Sie die Invariante in Zeile 31 auskommentieren und die Zeile 36 kommentieren und funktioniert.

Answer 1

Das Problem ist, dass Sie in der Definition von isABB Klammern fehlen.

Es sollte lauten:

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