我有 2 個函式，全部用于檢查 2 個序列中有多少個值具有相同的值和相同的索引，例如：

• 要求序列中沒有重復項 s:= [1,3,2,5,6] u:= [2,3,4,5,1]

==> bullspec(s,u) = 2

所以我的 2 個函式都回傳正確的值，但其中一個斷言為真，另一個為假這是我的 2 個函式：

function bullspec(s:seq<nat>, u:seq<nat>): nat
  requires 0 < |s| <= 10
  requires 0 < |u| <= 10
  requires |s| <= |u|
  // Remove duplicates
  requires forall i, j | 0 <= i < |s| && 0 <= j < |s| && i != j :: s[i] != s[j] && s[i] <= 10
  requires forall i, j | 0 <= i < |u| && 0 <= j < |u| && i != j :: u[i] != u[j] && u[i] <= 10
{
  if |s| == 1 then (
    if s[0] in u && s[0] == u[0] 
    then 1 else 0
  ) else (
    if s[|s|-1] in u && s[|s|-1]==u[|s|-1] 
    then (1   bullspec(s[..|s|-1], u))
    else bullspec(s[..|s|-1],u)
  )
}

和

function bullspec2(s:seq<nat>, u:seq<nat>): nat
  requires 0 < |s| <= 10
  requires 0 < |u| <= 10
  requires |s| <= |u|
  // Remove duplicates
  requires forall i, j | 0 <= i < |s| && 0 <= j < |s| && i != j :: s[i] != s[j] && s[i] <= 10
  requires forall i, j | 0 <= i < |u| && 0 <= j < |u| && i != j :: u[i] != u[j] && u[i] <= 10
{
  if |s| == 1 then (
    if s[0] in u && s[0] == u[0] 
    then 1 else 0
  ) else (
    if s[0] in u && s[0] == u[0]
    then (1   bullspec2(s[1..], u))
    else bullspec2(s[1..], u)
  )
}

我有一個主要的方法如下：

method Main()
{
  var sys:seq<nat> := [4,2,9,3,1];
  var usr:seq<nat> := [1,2,3,4,5];

  assert bullspec(sys, usr) == 1; //Assertion might not hold
  assert bullspec2(sys, usr) == 1; //This is good
}

兩個函式之間的區別在于回圈遞回，一個從頭開始，另一個從尾開始，并且以某種方式向后的 make assertion 作業得很好

我嘗試撰寫一些 ensures 陳述句，但沒有任何效果。

uj5u.com熱心網友回復：

首先，請注意您使用的是靜態分析器，而不是運行時測驗器。所以斷言可能在運行時成立，但靜態分析器無法證明它。靜態分析器可以證明第二個的事實已經相當驚人了。但我總是建議你改變斷言的順序，因為在第一個未經證實的斷言之后的斷言總是以未經證實的斷言為真為條件得到證明。你的情況，無論如何，它仍然bullspec無法解決。

它目前無法驗證的原因是尚未實作在不消耗燃料的情況下在存在序列文字的情況下間接評估序列長度的公理。看到這個類似的問題。這意味著，對于你的第二個例子，使用公理“評估”函式不會消耗“燃料”（我稍后會回到那個），但是對于第一個失敗的例子，它無法展開足夠的函式來進行計算.

你現在可以做的是：

創建一個引理并證明它（困難）

lemma bullspec2equalsBullspec(s:seq<nat>, u:seq<nat>): nat
  ensures  bullspec2(sys, usr) == bullspec(sys, usr)
{
  // TODO
}

然后寫：

assert bullspec2(sys, usr) == 1;
assert bullspec(sys, usr) == 1 by {
  bullspec2equalsBullspec(sys, usr);
}

在 bullspec 中將序列的長度作為 ghost 引數傳遞

function bullspec(s:seq<nat>, u:seq<nat>, length: nat): nat
  requires |s| == length
  requires 0 < |s| <= 10
  requires 0 < |u| <= 10
  requires |s| <= |u|
  // Remove duplicates
  requires forall i, j | 0 <= i < |s| && 0 <= j < |s| && i != j :: s[i] != s[j] && s[i] <= 10
  requires forall i, j | 0 <= i < |u| && 0 <= j < |u| && i != j :: u[i] != u[j] && u[i] <= 10
{
  if length == 1 then (
    if s[0] in u && s[0] == u[0] 
    then 1 else 0
  ) else (
    if s[length-1] in u && s[length-1]==u[length-1] 
    then (1   bullspec(s[..length-1], u,length-1))
    else bullspec(s[..length-1],u,length-1)
  )
}
/// ...
method Main()
{
  var sys:seq<nat> := [4,2,9,3,1];
  var usr:seq<nat> := [1,2,3,4,5];

  assert bullspec2(sys, usr) == 1; //This is good
  assert bullspec(sys, usr, 5) == 1; //This is good
}

驗證，因為現在它可以展開應用于文字的函式而無需燃料。

Unrollbullspec通過驗證除錯，看它阻塞在什么地方。

如果這個斷言應該成立，那么之前應該成立什么？您可以展開函式的定義并斷言中間結果。如果你斷言 Dafny 最終可以證明的一些不平凡的事情，那么剩下的一切都會被證明。我只展開了 3 個步驟的功能。

method Main()
{
  var sys:seq<nat> := [4,2,9,3,1];
  var usr:seq<nat> := [1,2,3,4,5];

  assert bullspec2(sys, usr) == 1; //This is good

  var sys1 := sys[..|sys|-1];
  var sys2 := sys1[..|sys1|-1];
  var sys3 := sys2[..|sys2|-1];
  var sys4 := sys3[..|sys3|-1];
  var sys5 := sys4[..|sys4|-1];

  assert bullspec(sys3, usr) == 1; 
  assert bullspec(sys2, usr) == 1; 
  assert bullspec(sys1, usr) == 1; 
  assert bullspec(sys, usr) == 1; //Assertion might not hold
}

為您的功能提供更多動力（最適合您的情況）

通過僅更改函式的定義，您可以為驗證程式實體化它提供更多燃料。對于您的情況，3 燃料就足夠了。

function {:fuel 10} bullspec(s:seq<nat>, u:seq<nat>): nat

標籤：测试达夫尼

上一篇：如何在SpringBootTest@Sql注解中使用掩碼描述檔案？

下一篇：Jmeter數學混淆