0

我正在尝试使用另一个谓词（即 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) 
}

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

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

fact chackJavaWellFormednessRules{
    checkOverriding[]
}

因此，我继续不理解错误：“没有要执行的命令”。

4

1 回答 1

3

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

如果你想让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但是如果模型中没有以or开头的子句，则模型中check没有“命令”。

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

于 2014-08-01T21:03:34.193 回答