我试图在Alloy中生成两组类,例如,重构应用程序之前的类和重构应用程序之后的类 . 假设在第一组中我们有以下类:
a -> br -> cr
class1
class2
意思是a是br的父级,而br又是cr,class1和class2的父级 .
另一方面,按照相同的推理,我们在第二组中有以下一组类:
a -> bl -> cl
class1
class2
类br,bl,cr和cl是实际参与重构的类 . 此外,br和bl实际上是相同的类(并且具有相同的标识),但是按照不同的时间顺序(不同的状态),以及cr和cl . 表示的重构是下推方法的简化,其中方法从br下推到cl类 .
下面给出了支持此转换的模型的简化:
open util/relation
abstract sig Id {}
sig ClassId, MethodId, FieldId extends Id {}
abstract sig Accessibility {}
one sig public, private_, protected extends Accessibility {}
abstract sig Type {}
abstract sig PrimitiveType extends Type {}
one sig Long_ extends PrimitiveType {}
abstract sig Class {
extend: lone ClassId,
methods: MethodId -> one Method,
fields: set Field
}
sig Field {
id: one FieldId,
type: one Type,
acc : one Accessibility,
}
sig Method {
return: lone Type,
acc: one Accessibility,
body: seq Statement
}
abstract sig Expression {}
abstract sig Statement{}
abstract sig PrimaryExpression extends Expression {
}
one sig this_, super extends PrimaryExpression {}
sig newCreator extends PrimaryExpression {
id_cf : one ClassId
}
sig MethodInvocation extends Statement{
pExp: one PrimaryExpression,
id_methodInvoked: one MethodId
}
sig Program {
classDeclarations: ClassId -> one Class
}
pred wellFormedProgram [p:Program] {
all c:ClassId | c in (p.classDeclarations).univ => wellFormedClass[p, c]
}
pred wellFormedClass[p:Program, c:ClassId] {
let class = c.(p.classDeclarations) {
all m:Method, mId:MethodId | m = mId.(class.methods) => wellFormedMethod[p, class, m, mId]
}
}
pred wellFormedMethod[p:Program, c:Class, m:Method, mId:MethodId]{
let body = (m.body).elems
{
all stm : Statement | stm in body => wellFormedStatement[p, c, stm]
}
}
pred wellFormedStatement[p:Program, c:Class, st:Statement]{
st in MethodInvocation => wellFormedMethodInvocation[p,c,st/*,m.param*/]
}
pred wellFormedMethodInvocation[p:Program, c:Class, stm: MethodInvocation] {
stm.pExp in PrimaryExpression => wellFormedPrimaryExpression[p, c, stm.pExp]
let target = stm.pExp {
target in newCreator => stm.id_methodInvoked in ((target.id_cf).(p.classDeclarations).*(extend.(p.classDeclarations)).methods).univ
target in this_ => stm.id_methodInvoked in (c.*(extend.(p.classDeclarations)).methods).univ
target in super => stm.id_methodInvoked in (c.^(extend.(p.classDeclarations)).methods).univ
}
}
pred wellFormedPrimaryExpression[p:Program, c:Class, stm: PrimaryExpression] {
stm in newCreator => classIsDeclared[p, stm.id_cf]
}
pred classIsDeclared[p:Program, c:ClassId] {
let cds = p.classDeclarations {
c in cds.univ
}
}
pred law14RL[b, c:ClassId, mId:MethodId, left, right: Program] {
wellFormedProgram[right]
let leftCds = left.classDeclarations,
rightCds= right.classDeclarations,
bl = b.leftCds,
br = b.rightCds,
cl = c.leftCds,
cr = c.rightCds,
mRight = mId.(br.methods),
mLeft = mId.(cl.methods)
{
mRight = mLeft
cr.extend = b
cl.extend = b
bl.extend = br.extend
leftCds = rightCds ++ {b -> bl} ++ {c -> cl}
all c:{Class - br - cl} | mId !in (c.methods).univ
cl.fields = cr.fields
bl.fields = br.fields
bl.methods = br.methods - {mId -> mRight}
cl.methods - {mId -> mLeft} = cr.methods
}
}
assert law14Prop {
all b, c:ClassId, mId:MethodId, left, right: Program |
law14RL[b, c, mId, left, right] implies wellFormedProgram[left]
}
check law14Prop for 15 but exactly 2 Program
看到谓词law14RL描述了转换本身以及b和c类的等价性(通过比较它们的方法和字段 - 在这个谓词的末尾) . 我们看到b类之间的唯一区别是br类中的mRight方法;类似地,方法mLeft存在于cl类中但不存在于cr类中 . 创建断言law14Prop是为了返回Alloy实例,该实例描述了由于方法的移动而导致编译错误问题(在转换的结果侧)的程序表示 .
例如,假设有一个方法m',其主体在br类中包含类似this.mId()的语句 . 如上所述,mId表示mRight方法的标识 . 该语句应该在bl类中引起编译错误,因为方法m'也存在于那里,但是由mId标识(方法mLeft)表示的方法是在cl类中 .
问题(问题)是这个模型没有返回任何反例,我不明白为什么 . 我究竟做错了什么?
奇怪的是,当我通过set Method(而不是MethodId - > Method)替换sig Class中的关系方法时 - 当然还要在模型中进行必要的修改 - 返回计数器示例 .
1 回答
这个问题存在于非常详细(并且涉及)的背景中,因此最好尝试分解它并缩小问题的潜在来源 .
这对我来说确实很奇怪,因为事实证明两个公式(以及一些额外的约束)确实应该表现相同,模仿你对模型做出的其他改变 . 我试图强制执行额外的约束,这些约束应该确实使两个公式相同(或者前者甚至更强),但我没有设法得到反例:
因此,可能是您所做的更改可能已经改变了模型的语义(并使其返回计数器示例) . 请注意,一种可能性是搜索域完全符合模型的一个公式而不适用于另一个公式(例如宇宙不足以在后一种情况下发现反例),但我怀疑这是这种情况 .
在任何情况下,我都建议尽可能缩小约束,直到求解器开始给出反例(再次,正如你所提到的) .