Dafny没有条件可触发谓词 [英] Dafny no terms to trigger on predicate

问题描述

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

I have the following snippet Dafny code for a tic tac toe game to check if player 1 has a winning row on the board:

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等）

Currently I am getting a /!\ No terms found to trigger on. error on the body of this predicate and all other predicates I have in my program (for winColumn, winDiag, ... etc)

如果有人可以帮助我解决此问题，我们将不胜感激

Would appreciate if someone can help me to fix this

推荐答案

这里是一种方法：引入一个辅助函数来容纳 forall 量词。然后，Dafny将使用此辅助函数作为外部 c量词的触发器，从而修正警告。

Here is one way to do it: introduce a helper function to hold the forall quantifier. Dafny will then use this helper function as the trigger for the outer exists quantifier, fixing the warning.

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)
}

请参见此答案以获取有关触发器的更多信息。

See this answer for more information about triggers.

这篇关于Dafny没有条件可触发谓词的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！