如何在 Alloy 中构建递归谓词/函数 [英] How to build recursive predicates/functions in Alloy

问题描述

我试图在 Alloy 中生成两组类，例如，重构前的类重构应用程序后的应用程序和类.假设在第一组中我们有以下类:

I am trying to generate in Alloy two sets of classes, for instance, classes before a refactoring application and classes after a refactoring application. Suppose in the first set we have the following classes:

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

意味着 ALeft 是 BLeft 的父级，而 BLeft 又是 CLeft、Class1 和Class2，又是 Class3 和 Class4 的父级.

meaning that ALeft is the parent of BLeft which in turn is the parent of CLeft, Class1 and Class2, which in turn is the parent of Class3 and Class4.

另一方面，按照同样的推理，我们在第二组以下班级:

On the other hand, following the same reasoning, we have in the second set the following group of classes:

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

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

Since each set represent the same classes but in different chronological order (different states), it is necessary to guarantee the corresponding equivalences, such as Class1 and Class1' are equivalent meaning that they have the same fields, methods, and so on (consider that the refactoring occurs only in B and C classes) . For the same reasoning, Class2 and Class2', Class3 and Class3', Class4 and Class4' are also equivalent. In addition, we should have an equivalence among the methods in Left and Right classes. For instance, if we have a Left class method like:

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

那么，一定有对应的Right类方法如:

Then, there must be a corresponding Right class method like:

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

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

As suggested by Loic (in this discussion list), the equivalence of these classes started to be guaranteed but we have to complement the predicate classesAreTheSame below, in order to also guarantee the equivalence of their methods. Consider the model below:

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 不允许递归，并且在使用传递闭包时会丢失与排序相同的继承级别.知道我如何在合金中表示这个吗?

My idea was identifying the corresponding methods (leftClassMethod() and rightClassMethod()) through their ids (which is guaranteed to be the same, according to the model). However, the predicate equalsSeqComposition is not working and the situation gets worse when i try to include the rest relation of the signature SequentialComposition in comparison (commented above in the predicate equalsSeqComposition). This last comparison is even more difficult since Alloy do not allow recursion and the same levels of inheritence as ordering is lost when you use transitive closure. Any idea how can i represent this in Alloy?

推荐答案

只有在递归深度不超过 3 时，才有可能在 Alloy 中递归调用函数和谓词 3 参见:在合金中编程递归函数

It is possible to call functions and predicate recursively in Alloy only if the recursion depth does not exeed 3 see : Programming recursive functions in alloy

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

For your problem, You can emulate the recursion you are trying to specify using the transitive closure operator.

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

I would rewrite your predicate classesAreTheSameAndSoAreTheirCorrespondingSons as follows :

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 是相同的，并且任何 r/l 继承(直接或间接)right/left 的类在 l/r 继承(直接或间接)的类中有一个对应部分分别为左/右.

This predicate enforces that the two classes right and left given are the same, and that any classes r/l inheriting (directly or indirectly) right/left has one counter part in the classes l/r inheriting (directly or indirectly) left/right , respectively.

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

The checkclassesAreTheSame[r.extend ,l.extend] is meant to check that r and l are in the same levels of inheritence as ordering is lost when you use transitive closure.

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

Here is the small model I designed to play with your problem :

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

祝其他人好运;)

这篇关于如何在 Alloy 中构建递归谓词/函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！