代码之家 › 专栏 › 技术社区 › Tarciana

在Alloy中使用谓词

predicates alloy reusability function

0

Tarciana · 技术社区 · 11 年前

我试图使用另一个谓词(即checkOverride)中的两个谓词(例如,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·斯佩伯格-麦昆先生,但我认为我的问题不够清楚。

我的谓词,比如checkOverride,是从如下事实调用的:

fact chackJavaWellFormednessRules{
    checkOverriding[]
}

因此,我仍然不理解错误:“没有要执行的命令”。

1 回复 | 直到 11 年前

1

3

C. M. Sperberg-McQueen 11 年前

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

如果您希望Analyzer执行任何操作,则需要向它发出指令;搜索谓词实例的指令是 run 。所以你会想说

run methodsWithSameParameters for 3

或

run methodsWithSameParameters for 5
run methodsWithSameReturn for 5

注意,在Alloy模型中可以有多个指令;Analyzer允许您告诉它执行哪个。

[附录]

合金分析仪关注关键词 跑 和 check (并且只有它们)作为“命令”。从您的描述中,听起来很像是在模型中没有出现这些关键字。

如果您只想查看Alloy模型的一些实例(以验证模型不是自相矛盾的),那么最简单的方法是向模型中添加以下内容:

pred show {}
run show for 3

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

run checkOverriding

但在模型中没有以 跑 或 检查 ,模型中没有“命令”。

你说你已经定义了一个谓词( checkOverriding )然后在总是满足该谓词的事实中指定。这相当于说谓词 检查覆盖 总是正确的 检查覆盖 事实而不是谓词),但它具有纯粹的声明性含义,不算作“命令”。如果希望Alloy查找谓词的实例,则必须使用 跑 命令如果希望Alloy查找断言的反例,则必须使用 检查 命令