triggers - Dafny 没有条件可以触发谓词

Question

我有以下用于 tic tac toe 游戏的 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、...等)

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

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有关触发器的更多信息。