Dafny 没有在谓词上触发的条件

Question

我有以下用于井字游戏的 sn-p Dafny 代码，用于检查玩家 1 在棋盘上是否有获胜行：

predicate isWinRowForPlayer1(board: array2<int>)
  reads board
  requires board.Length0 == board.Length1 == 3 && isValidBoard(board)
{
  exists i :: 0 <= i < board.Length0 ==> (forall j :: 0 <= j < board.Length1 ==> board[i, j] == 1)
}

目前我在这个谓词的主体和我的程序中的所有其他谓词（对于 winColumn、winDiag、...等）的主体上收到 /!\ No terms found to trigger on. 错误

如果有人能帮我解决这个问题，我们将不胜感激

Answer 1

这是一种方法：引入一个辅助函数来保存forall 量词。然后，Dafny 将使用此辅助函数作为外部 exists 量词的触发器，修复警告。

predicate RowIsWinRowForPlayer1(board: array2<int>, row: int)
    reads board
    requires 0 <= row < board.Length0
{
    forall j :: 0 <= j < board.Length1 ==> board[row, j] == 1
}

predicate isWinRowForPlayer1(board: array2<int>)
  reads board
  requires board.Length0 == board.Length1 == 3 && isValidBoard(board)
{
  exists i :: 0 <= i < board.Length0 ==> RowIsWinRowForPlayer1(board, i)
}

有关触发器的更多信息，请参阅this answer。