在合金中使用谓词

Question

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

正如我在之前的一些问题中所评论的，它们是 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

您已经定义了谓词；它们具有纯粹的声明性语义，它们在模型实例的某些子集中为真，在互补子集中为假。

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

run methodsWithSameParameters for 3

或

run methodsWithSameParameters for 5
run methodsWithSameReturn for 5

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

---

[附录]

Alloy Analyzer 将关键字 run 和 check（并且只有它们）视为“命令”。根据您的描述，听起来好像您在模型中没有出现任何这些关键字。

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

pred show {}
run show for 3

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

run checkOverriding 

但如果模型中没有以 run 或 check 开头的子句，则模型中没有“命令”。

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