如何在 Alloy 中构建递归谓词/函数

Question

我正在尝试在 Alloy 中生成两组类，例如，重构之前的类 重构应用程序后的应用程序和类。 假设在第一组中我们有以下类：

ALeft -> BLeft -> CLeft    
                  Class1
                  Class2 -> Class3
                         -> Class4

表示 ALeft 是 BLeft 的父级，而 BLeft 又是 CLeft、Class1 和 Class2，它又是 Class3 和 Class4 的父级。

另一方面，按照同样的推理，我们在第二组中 以下组类：

ARight -> BRight -> CRight
                    Class1'
                    Class2' -> Class3'
                            -> Class4'

由于每个集合代表 相同的类但按不同的时间顺序（不同的状态），有必要保证相应的 等价，例如 Class1 和 Class1' 是等价的，意味着它们具有相同的字段、方法等（考虑重构仅发生 在 B 和 C 类）。同理，Class2 和 Class2'、Class3 和 Class3'、Class4 和 Class4' 也是等价的。此外，我们应该在 Left 和 Right 类中的方法之间具有等价性。例如，如果我们有一个 Left 类方法，例如：

public int leftClassMethod(){
    new ALeft().other();
}

那么，就必须有一个对应的Right类方法，比如：

public int rightClassMethod(){
    new ARight().other();
}

正如 Loic 所建议的（在这个讨论列表中），这些类的等价性开始得到保证，但我们必须补充下面的谓词 classesAreTheSame，以便也保证它们的方法的等价性。考虑以下模型：

abstract sig Id {}

sig ClassId, MethodId,FieldId extends Id {}

one sig public, private_, protected extends Accessibility {}

abstract sig Type {}

abstract sig PrimitiveType extends Type {}

one sig Long_, Int_ extends PrimitiveType {}

sig Class extends Type {
    id: one ClassId,
    extend: lone Class,
    methods: set Method,
    fields: set Field,
}

sig Method {
    id : one MethodId,
    param: lone Type,
    return: one Type,
    acc: lone Accessibility,
    b: one Block
}

sig Block {
    statements: one SequentialComposition
}

sig SequentialComposition {
    first: one StatementExpression,
    rest: lone SequentialComposition
}

abstract sig Expression {}
abstract sig StatementExpression extends Expression {}

sig MethodInvocation extends StatementExpression{
    pExp: lone PrimaryExpression, 
    id_methodInvoked: one Method
}

sig AssignmentExpression extends StatementExpression {
    pExpressionLeft: one FieldAccess,
    pExpressionRight: one {Expression - newCreator - VoidMethodInvocation - PrimaryExpression - AssignmentExpression }
}

abstract sig PrimaryExpression extends Expression {}

sig this_, super_ extends PrimaryExpression {}

sig newCreator extends PrimaryExpression {
    id_cf : one Class
}

sig FieldAccess {
    pExp: one PrimaryExpression,
    id_fieldInvoked: one Field
}

sig Left,Right extends Class{}

one sig ARight, BRight, CRight extends Right{}

one sig ALeft, BLeft, CLeft extends Left{}

pred law6RightToLeft[] {
    twoClassesDeclarationInHierarchy[]
}

pred twoClassesDeclarationInHierarchy[] {
     no disj x,y:Right | x.id=y.id
     Right.*extend & Left.*extend=none
     one r: Right | r.extend= none
     one l:Left| l.extend=none

     ARight.extend=none
     ALeft.extend=none
     BRight in CRight.extend
     BLeft in CLeft.extend
     ARight in BRight.extend
     ALeft in BLeft.extend
     #(extend.BRight) > 2
     #(extend.BLeft) > 2
     #(extend.ARight) = 1
     #(extend.ALeft) = 1
     CLeft.id=CRight.id

     all m:Method | m in ((*extend).ALeft).methods => m !in ((*extend).ARight).methods
     all m:Method | m in ((*extend).ARight).methods => m !in ((*extend).ALeft).methods
     some Method
     all r:Right | all l:Left|  (r.extend= none and l.extend=none) implies classesAreTheSameAndSoAreTheirCorrespondingSons[r,l]
}

pred classesAreTheSameAndSoAreTheirCorrespondingSons[right,left: Class]{
    classesAreTheSame[right,left]
    all r: right.^~extend | one l :left.^~extend | classesAreTheSame[r,l] and classesAreTheSame[r.extend ,l.extend]
    all l:left.^~extend | one r :right.^~extend | classesAreTheSame[r,l] and  classesAreTheSame[r.extend ,l.extend]
}

pred classesAreTheSame[r,l: Class]{
    r.id=l.id
    r.fields=l.fields

    #r.methods = #l.methods
    all mr: r.methods | one ml: l.methods | mr.id = ml.id && mr.b != ml.b 
    all mr: l.methods | one ml: r.methods | mr.id = ml.id && mr.b != ml.b 

    all r1: r.methods, r2: l.methods | r1.id = r2.id => 
        equalsSeqComposition[r1.b.statements, r2.b.statements]
}

pred equalsSeqComposition[sc1, sc2: SequentialComposition]{
    equalsStatementExpression[sc1.first, sc2.first] 
    //#sc1.(*rest) = #sc2.(*rest)
}

pred equalsStatementExpression [s1, s2: StatementExpression]{
    s1 in AssignmentExpression => (s2 in AssignmentExpression && equalsAssignment[s1, s2])
    s1 in MethodInvocation => (s2 in MethodInvocation && equalsMethodInvocation[s1, s2])
    s1 in VoidMethodInvocation => (s2 in VoidMethodInvocation && equalsVoidMethodInvocation[s1, s2])
}

pred equalsAssignment [ae, ae2:AssignmentExpression]{
    equalsPrimaryExpression[(ae.pExpressionLeft).pExp, (ae2.pExpressionLeft).pExp]
    equalsPExpressionRight[ae.pExpressionRight, ae2.pExpressionRight]
}

pred equalsPrimaryExpression[p1, p2:PrimaryExpression]{
    p1 in newCreator  => p2 in newCreator && equalsClassesId [p1.id_cf, p2.id_cf]
    p1 in this_ => p2 in this_ 
    p1 in super_ => p2 in super_
}

pred equalsPExpressionRight[e1, e2:Expression]{
    e1 in LiteralValue => e2 in LiteralValue 
    e1 in MethodInvocation => e2 in MethodInvocation && equalsMethodInvocation[e1, e2]
}

pred equalsMethodInvocation[m1, m2:MethodInvocation]{
    equalsPrimaryExpression[m1.pExp, m2.pExp]
    m1.id_methodInvoked.id = m2.id_methodInvoked.id 
    m1.param = m2.param
}

pred equalsVoidMethodInvocation[m1, m2:VoidMethodInvocation]{
    equalsPrimaryExpression[m1.pExp, m2.pExp]
    m1.id_voidMethodInvoked.id = m2.id_voidMethodInvoked.id
    m1.param = m2.param
}

run law6RightToLeft for 10 but 17 Id, 17 Type, 17 Class

我的想法是通过它们的 id 识别相应的方法（leftClassMethod() 和 rightClassMethod()）（根据模型，这保证是相同的）。但是，谓词 equalsSeqComposition 不起作用，并且当我尝试将签名 SequentialComposition 的其余关系包含在内时情况会变得更糟（在谓词 equalsSeqComposition 中已在上面进行了评论）。最后一个比较更加困难，因为 Alloy 不允许递归，并且当您使用传递闭包时，与排序相同的继承级别会丢失。知道如何在 Alloy 中表示这一点吗？

Answer 1

只有在递归深度不超过 3 的情况下，才可以在 Alloy 中递归调用函数和谓词，请参阅：Programming recursive functions in alloy

对于您的问题，您可以使用传递闭包运算符模拟您尝试指定的递归。

我会重写你的谓词classesAreTheSameAndSoAreTheirCorrespondingSons 如下：

pred classesAreTheSameAndSoAreTheirCorrespondingSons[right,left: Class]{
    classesAreTheSame[right,left]
    all r: right.^~extend | one l :left.^~extend | classesAreTheSame[r,l] and classesAreTheSame[r.extend ,l.extend]
    all l:left.^~extend | one r :right.^~extend | classesAreTheSame[r,l] and  classesAreTheSame[r.extend ,l.extend]
}

这个谓词强制给定的两个类 right 和 left 是相同的，并且任何继承（直接或间接） right/left 的类 r/l 在继承（直接或间接）的类 l/r 中都有一个对应部分分别是左/右。

checkclassesAreTheSame[r.extend ,l.extend] 用于检查 r 和 l 是否处于相同的继承级别，因为使用传递闭包时会丢失排序。

这是我为解决您的问题而设计的小型模型：

abstract sig Class {
    id: Int,
    extend: lone Class
}{
   this not in this.^@extend
}

sig Left,Right extends Class{}

fact{
     no disj x,y:Right | x.id=y.id
     Right.*extend & Left.*extend=none 
     one r: Right | r.extend= none 
     one l:Left| l.extend=none
     all r:Right | all l:Left|  (r.extend= none and l.extend=none) implies classesAreTheSameAndSoAreTheirCorrespondingSons[r,l]    
}

pred classesAreTheSameAndSoAreTheirCorrespondingSons[right,left: Class]{
    classesAreTheSame[right,left]
    all r: right.^~extend | one l :left.^~extend | classesAreTheSame[r,l] and classesAreTheSame[r.extend ,l.extend]
    all l:left.^~extend | one r :right.^~extend | classesAreTheSame[r,l] and  classesAreTheSame[r.extend ,l.extend]
}

pred classesAreTheSame[r,l: Class]{
    r.id=l.id
}
run {} for exactly 10 Class

祝你好运；）