考虑解决100 名囚犯和一个灯泡问题的标准策略。这是我在 Dafny 中对其建模的尝试:
method strategy<T>(P: set<T>, Special: T) returns (count: int)
requires |P| > 1 && Special in P
ensures count == (|P| - 1)
decreases *
{
count := 0;
var I := {};
var S := {};
var switch := false;
while (count < (|P|-1))
invariant count <= (|P|-1)
invariant count > 0 ==> Special in I
invariant Special !in S && S < P && S <= I && I <= P
decreases *
{
var c :| c in P;
I := I + {c};
if c == Special {
if switch == true {
switch := false;
count := count + 1;
}
} else {
if c !in S && switch == false {
S := S + {c};
switch := true;
}
}
}
assert(I == P);
}
然而,它最终无法证明这一点I == P
。为什么?我可能需要进一步加强循环不变量,但无法想象从哪里开始......