2

我试图在 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 实例，这些实例描述了由于方法的移动而具有编译错误问题（在转换的结果侧）的程序表示。

例如，假设在 br 类中有一个方法m'，其主体包含类似this.mId()的语句。如前所述，mId表示mRight方法的标识。该语句应该会导致 bl 类中的编译错误，因为方法m'也存在于那里，但由mId标识表示的方法（方法 mLeft）却在 cl 类中。

关键（问题）是这个模型没有返回任何反例，我不明白为什么。我究竟做错了什么？

奇怪的是，当我用 set Method （而不是 MethodId -> Method ）替换 sig Class 中的关系方法时-当然在模型中进行所需的修改 - 返回反例。

4

1 回答 1

2

这个问题位于一个非常详细（且涉及）的上下文中，因此最好尝试分解它并缩小问题的潜在来源。

奇怪的是，当我用 set Method （而不是 MethodId -> Method）替换 sig Class 中的关系方法时 - 当然在模型中进行所需的修改 - 返回反例。

这对我来说也确实很好奇，因为事实证明这两个公式（连同一些额外的约束）确实应该表现相同，以您对模型所做的其他更改为模。我试图强制执行额外的约束，这些约束确实应该使这两个公式等效（或者可能前者更强大），但我没有设法得到反例：

// all method Ids must map to same actual methods
fact methodsIdUnique {
    all a,b: Class, mId: MethodId |
        all m1: mId.(a.methods) |
        all m2: mId.(b.methods) |
        m1 = m2
}

// there cannot be two different Ids that map to the same method
fact methodsIdUnique {
    all a: Class, mId1: MethodId, mId2: MethodId, m: Method |
        m = mId1.(a.methods) && m = mId2.(a.methods) implies
            mId1 = mId2
}

// this is too strong, wrt to your description
fact methodsExist {
    all a,b: Class, mId: MethodId |
        some mId.(a.methods) &&
        some mId.(b.methods)
}

因此，您所做的更改可能会改变模型的语义（并使其返回反例）。请注意，一种可能性也是搜索域完全适合模型的一种公式，但不适合另一种公式（例如，宇宙不够大，无法在后一种情况下发现反例），但我怀疑这里的情况。

无论如何，我建议尽可能缩小约束，直到求解器开始给出反例（再次，正如你提到的）。

于 2016-09-25T19:44:11.130 回答