나는 합금에서 두 세트의 클래스, 예를 들어 리팩토링 이전의 클래스와 리펙토링 어플리케이션 이후의 클래스를 생성하려고한다. 우리는 다음과 같은 클래스가 첫 세트에서 가정 :합금의 매핑 다루기
a -> br -> cr
class1
class2
을 A가 차례로 CR, 클래스 1과 Class2의의 부모 인 BR의 부모는 것을 의미한다. 같은 추론 다음 한편
, 우리는 두 번째 세트에서 클래스의 다음과 같은 그룹이 있습니다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
이 변환을 지원하는 모델의 단순화는 다음과 주어진다 필드 -이 술어 끝에 있음). b 클래스 간의 유일한 차이점은 메소드 mRight 인 br 클래스에 있음을 알 수 있습니다. 마찬가지로, mLeft 메서드는 cl 클래스에는 있지만 cr 클래스에는 존재하지 않습니다. 이 어설 션 law14Prop은 메소드 이동으로 인한 변환 오류가있는 프로그램 표현을 나타내는 Alloy 인스턴스를 반환하기 위해 만들어졌습니다.
는 예를 들어, 본문 this.mId 같은 문을 포함하는 방법 m ',()는 BR 클래스에서,이 가정합니다. 진술 한 바와 같이, mId은 mRight 방법의 식별을 나타낸다. 이 문은 m '도 존재하기 때문에 bl 클래스에서 컴파일 오류가 발생해야하지만 mId 식별 (메서드는 mLeft)으로 표시되는 메서드는 cl 클래스에 대신 있습니다.
요점 (문제)은이 모델이 어떠한 반대 사례도 반환하지 않고 그 이유를 이해하지 못한다는 것입니다. 내가 도대체 뭘 잘못하고있는 겁니까? 난 하여 관계를 방법SIG 클래스에 조립할 때
흥미롭게 방법 세트 (대신 MethodId 중 -> 방법) - 물론 모델의 필요한 수정 않는다 - 이의 예로는 리턴 .