2

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:

a -> br -> cr
           class1
           class2

meaning that a is the parent of br which in turn is the parent of cr, class1 and class2.

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

a -> bl -> cl 
           class1
           class2

Classes br, bl, cr and cl are the ones that actually participate of the refactoring. In addition, br and bl are actually the same classes (and have the same identification) but in different chronological order (different states), as well as cr and cl. The refactoring being represented is a simplification of the pushing down method, where a method is pushed down from br to cl class.

A simplification of the model that supports this transformation is given below:

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

See that the predicate law14RL describes the transformation itself and the equivalence of the b and c classes (by comparing their methods and fields - at the end of this predicate). We see that the only difference between b classes is the method mRight in br class; similarly, the method mLeft exists in cl class but not in cr class. The assertion law14Prop was created in order to return Alloy instances that depicts programs representations with compilation-errors problems (in the resulting side of the transformation) due to the moving of the method.

For instance, suppose there is a method m', whose body contains a statement like this.mId(), in the br class. As stated, mId represents the identification of the mRight method. This statement should cause a compilation error in the bl class since the method m' also exists there but the method represented by mId identification (the method mLeft) is in the cl class instead.

The point (problem) is that this model is not returning any counter examples and i am not understanding why. What am i doing wrong?

Curiously, when i replace the relation methods in sig Class by set Method (instead of MethodId -> Method) - and of course do the required modifications in the model - counter examples are returned.

Tarciana
  • 113
  • 10

1 Answers1

2

This question lies within a pretty detailed (and involved) context, so it would be probably best to try to decompose it and narrow down the potential sources of the issue.

Curiously, when i replace the relation methods in sig Class by set Method (instead of MethodId -> Method) - and of course do the required modifications in the model - counter examples are returned.

This is indeed curious to me as well, as it turns out that the two formulations (together with some additional constraints) should indeed behave the same, modulo other changes you made to your model. I've tried to enforce additional constraints that should indeed make the two formulations equivalent (or perhaps the former even stronger), but I did not manage to get counter examples:

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

Thus, it might be the case that the changes you've made, might have changed the semantics of the model (and make it return counter examples). Note that one possibility is also that the domain of search exactly fits one formulation of the model but not the other (thus e.g. the universe is not big enough to discover counter examples in the latter case), but I doubt this is the case here.

In any case, I would suggesting narrowing the constraints as much as possible until the solver starts giving counter examples (again, as you mentioned).

ivcha
  • 463
  • 5
  • 15