合金表达式类型检查失败

Question

我是 Alloy（规范语言）的初学者，需要根据案例研究做一些进一步的工作，案例研究可以在这里找到（代码在第 5 页）。相关代码：

open util/ordering[Time] as T0

pred Eavesdropping() {   
  some pro:Process | some m:Protected_Msg |  
  some t: (Time - T0/last) - T0/prev[T0/last] |   let t' = T0/t.next |
  let t'' = T0/t'.next |   !HasReadAccess[pro,m] && (m->t in pro.knows)
  &&   (m.contents->t not in pro.knows) &&   (m.contents->t'' in
  pro.knows) && IsUnique(m.contents) }

更正一些语法后，我收到此错误消息：“此表达式无法进行类型检查”，并t'以let t' = T0/t.next. 我如何打字t'？

Answer 1

这里的错误是 next 是别名所引用的模块中的一个函数T0，所以 let 绑定的 RHS 上的表达式应该是t.T0/next而不是T0/t.next。但实际上您无论如何都不需要T0，因为 Alloy 可以确定正在引用哪个模块。因此，只需删除对的所有引用T0，它应该可以正常编译。

另一条评论：您可以删除所有这些连词符号并使用隐式连词，写作

{ A B C }

而不是A && B && C.