1

我是 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'？

4

1 回答 1

5

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

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

{ A B C }

而不是A && B && C.

于 2011-11-16T02:29:45.470 回答