处理 Alloy 中的映射

Question

我试图在 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 类中而是。

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

奇怪的是，当我将 sig Class 中的关系 methods 替换为 set Method （而不是 MethodId -> Method em>) - 当然在模型中进行必要的修改 - 返回反例。

Answer 1

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

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

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

// 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)
}

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

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