在 Alloy 中使用谓词

Question

我试图使用另一个谓词（即，methodsWiThSameParameters 和methodsWiThSameReturn）的两个谓词（即checkOverriding），但我收到以下错误：“没有要执行的命令”。有什么线索吗？我也尝试使用函数，但没有成功，要么是由于语法，要么是函数不返回布尔值。

正如我在之前的一些问题中评论的那样，它们是 Alloy 中指定的 java 元模型的一部分。

pred checkOverriding[]{
//check accessibility of methods involved in overriding
  no c1, c2: Class {
    c1=c2.^extend
    some m1, m2:Method |
          m1 in c1.methods && m2 in c2.methods && m1.id = m2.id 
          && methodsWiThSameParameters[m1, m2] && methodsWiThSameReturn[m1, m2] && 
               ( (m1.acc = protected && (m2.acc = private_ || #(m2.acc) = 0 )) ||
                 (m1.acc = public && (m2.acc != public || #(m2.acc) = 0 )) ||
                 (#(m1.acc) = 0 && m2.acc != private_ )
               )
      }
    }

pred methodsWiThSameParameters [first,second:Method]{
    m1.param=m2.param || (#(m1.param)=0 && #(m2.param)=0)  
}
pred methodsWiThSameReturn [first, second:Method]{
    m1.return=m2.return || (#(m1.return)=0 && #(m2.return)=0) 
}

---

谢谢您的回复，C 先生。M。Sperberg-McQueen，但我认为我的问题不够清楚。

我的谓词，比如 checkOverriding，是从这样的事实中调用的：

fact chackJavaWellFormednessRules{
    checkOverriding[]
}

因此，我仍然不理解这个错误：“没有要执行的命令”。

Answer 1

您已经定义了谓词；它们具有纯粹的声明性语义，并且它们在模型实例的某些子集中为 true，而在补充子集中为 false。

如果你想让分析器做任何事情，你需要给它一个指令；搜索谓词实例的指令是 run. 。所以你会想说类似的话

run methodsWithSameParameters for 3

或者

run methodsWithSameParameters for 5
run methodsWithSameReturn for 5

请注意，合金模型中可以有多个指令；分析器让您告诉它要执行哪个。

---

[附录]

合金分析仪关注关键词 run 和 check （并且只有他们）作为“命令”。从您的描述来看，听起来好像模型中没有出现这些关键字。

如果您只想查看 Alloy 模型的一些实例（以验证该模型不自相矛盾），那么最简单的方法就是在模型中添加如下内容：

pred show {}
run show for 3

或者，如果您已经有一个命名谓词，您可以简单地添加一个 run 该谓词的命令：

run checkOverriding 

但模型中没有以以下任一开头的子句 run 或者 check, ，模型中没有“命令”。

你说你已经定义了一个谓词（checkOverriding），然后在事实中指定该谓词始终满足。这相当于说谓词 checkOverriding 总是正确的（并且也可以通过使 checkOverriding 事实而不是谓词），但它具有纯粹的声明性含义，并且不能算作“命令”。如果您希望 Alloy 查找谓词的实例，则必须使用 run 命令;如果你想让 Alloy 找到断言的反例，你必须使用 check 命令。