在Dafny中遍历无限映射（imap）时如何指定范围？

Dafny 4.0及以上版本对非幽灵上下文的imap推导增加了编译可验证性要求，你遇到的报错是因为原代码中的imap推导没有明确指定有界的遍历范围，编译器无法确定需要处理的键集合。

针对你的场景，and和or函数只需要处理输入两个imap的键的并集——不在这个集合中的键不会影响sat谓词的结果，因此可以明确限定遍历范围为x.Keys ∪ y.Keys，修改后的代码如下：

type temporal = imap<int, bool>
type Behavior<S> = imap<int, S>
    
function stepmap(f:imap<int, bool>):temporal
  ensures  forall i:int :: i in f ==> sat(i, stepmap(f)) == f[i]
{
  f
}

predicate sat(s:int, t:temporal)
{
  s in t && t[s]
}

function{:opaque} and(x:temporal, y:temporal):temporal
  ensures  forall i:int {:trigger sat(i, and(x, y))} :: sat(i, and(x, y)) == (sat(i, x) && sat(i, y))
{
  stepmap(imap i in x.Keys ∪ y.Keys :: sat(i, x) && sat(i, y))
}

function{:opaque} or(x:temporal, y:temporal):temporal
  ensures  forall i:int {:trigger sat(i, or(x, y))} :: sat(i, or(x, y)) == (sat(i, x) || sat(i, y))
{
  stepmap(imap i in x.Keys ∪ y.Keys :: sat(i, x) || sat(i, y))
}

修改说明 #

• 在imap推导中添加i in x.Keys ∪ y.Keys，明确告诉编译器遍历的键集合是两个输入imap的键的并集，这个集合是有界且可编译的。
• 该修改完全符合原代码的逻辑：对于不在x.Keys ∪ y.Keys中的i，sat(i, and(x,y))为false，sat(i,x) && sat(i,y)也为false；or函数同理，依然满足原有的ensures条件。

内容的提问来源于stack exchange，提问作者ZihaoZhang