合金表达式无法进行类型检查答案

【问题标题】：Alloy expression failed to be typechecked合金表达式无法进行类型检查
【发布时间】：2011-11-15 21:01:23
【问题描述】：

我是 Alloy（规范语言）的初学者，需要根据案例研究做一些进一步的工作，可以找到 here（代码在第 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) }

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

【问题讨论】：

标签： logic modeling specifications first-order-logic alloy

【解决方案1】：

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

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

{ A B C }

而不是A && B && C。

【讨论】：