這是 Bulls and Cows 游戲的代碼，簡單地說就是我們有 2 個長度相同的陣列 a[] 和 b[]，如果 a[i] == b[i] 那么 Bulls = 1，如果 a[i ] 在 b && a[i] != b[i] 然后 Cows = 1。
我已經撰寫了 Bulls 和 Cows 函式，但是 BullCows 方法在計算時有一些問題，它使我的斷言失敗。
`
function bullspec(s:seq<nat>, u:seq<nat>): nat
requires |s| > 0
requires |u| > 0
requires |s| == |u|
{
var index:=0;
if |s| == 1 then (
if s[0]==u[0]
then 1 else 0
) else (
if s[index] != u[index]
then bullspec(s[index 1..],u[index 1..])
else 1 bullspec(s[index 1..],u[index 1..])
)
}
function cowspec(s:seq<nat>, u:seq<nat>): nat
requires |s| > 0
requires |u| > 0
requires |s| <= |u|
{
var extra:= |u|-|s|;
var index:=0;
if |s| == 1 then (
if s[0] in u
then 1 else 0
) else(
if s[index] in u && s[index]!=u[extra]
then (1 cowspec(s[index 1..],u))
else cowspec(s[index 1..],u)
)
}
method BullsCows (s:seq<nat>, u:seq<nat>) returns (b:nat, c:nat)
requires |s|>0 && |u|>0 &&|s|==|u|
// No duplicates in array
requires forall i, j | 0 <= i < |s| && 0 <= j < |s| && i != j :: s[i] != s[j]
requires forall i, j | 0 <= i < |u| && 0 <= j < |u| && i != j :: u[i] != u[j]
ensures forall k :: 0 <= k < |s| && s[k] !in u ==> b == c == 0
ensures forall k :: 0 <= k < |s| && s[k] in u ==> (c b) > 0
{
var index := 0;
b := 0;
c := 0;
while(index<|s|)
invariant index <= |s|
invariant forall k :: 0 <= k < index && s[k] in u ==> (b c) > 0
{
if s[index] in u {
if s[index] == u[index]{
b:=b 1;
} else {
c:=c 1;
}
}
index:=index 1;
}
}
method NotMain()
{
var sys:seq<nat> := [4,2,9,3,1];
var usr:seq<nat> := [1,2,3,4,5];
assert bullspec(sys, usr) == 1; //True
assert cowspec(sys, usr) == 3; //True
var b:nat, c:nat := BullsCows(sys, usr);
assert b == 1; //Not true
assert c == 3; //Not true
}
` NotMain 方法表示 assert b == 1; 并斷言 c==3；不是真的，這是 Dafny 的語言，請有人能幫我解決這個邏輯問題，我在敲我的頭。
我嘗試在 BullsCows 方法中設定許多確保但沒有任何反應
uj5u.com熱心網友回復：
問題是 on 的后置條件BullsCows()不足以證明最后兩個斷言。BullsCows()特別是， 和 的操作與規范bullspec()和之間沒有聯系cowspec()。你需要把這些東西聯系在一起。
為了說明，我將使用一個更容易理解的簡單示例。對于上面的示例，最終斷言在以下方面失敗：
function sumspec(xs: seq<nat>, i: nat) : nat
requires i <= |xs| {
if |xs| == 0 || i == 0 then 0
else sumspec(xs,i-1) xs[i-1]
}
method sum(s:seq<nat>) returns (r:nat) {
r := 0;
for i := 0 to |s| {
r := r s[i];
}
return r;
}
method main() {
assert sumspec([1,2,3],3) == 6;
var r := sum([1,2,3]);
assert r == 6;
}
雖然sumspec()這是一個有效的規范，因為sum()我們還沒有將這兩件事聯系起來。因此，Dafny 假設sum()可以回傳任何值r！
為了將規范 ( sumspec) 與其實作 ( sum) 聯系起來，我們需要一個更強的后置條件：
method sum(s:seq<nat>) returns (r:nat)
ensures r == sumspec(s,|s|) {
r := 0;
for i := 0 to |s|
invariant r == sumspec(s,i) {
r := r s[i];
}
return r;
}
在這里，r == sumspec(s,|s|)將規范與我們的實施結果聯系起來。我們還添加了一個回圈invariant來幫助 Dafny 證明這個后置條件成立。
轉載請註明出處，本文鏈接：https://www.uj5u.com/yidong/535628.html
標籤：测试达夫尼