我正在为 Java 的一个子集做一个合金元模型。
下面我们有一些签名:
abstract sig Id {}
sig Package{}
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 Int_, Long_ extends PrimitiveType {}
sig Class extends Type {
package: one Package,
id: one ClassId,
extend: lone Class,
methods: set Method,
fields: set Field
}
sig Field {
id : one FieldId,
type: one Type,
acc : lone Accessibility
}
sig Method {
id : one MethodId,
param: lone Type,
acc: lone Accessibility,
return: one Type,
b: one Body
}
abstract sig Body {}
sig LiteralValue extends Body {} // returns a random value
abstract sig Qualifier {}
one sig this_, super_ extends Qualifier {}
sig MethodInvocation extends Body {
id_methodInvoked : one Method,
q: lone Qualifier
}
// return new A().k();
sig ConstructorMethodInvocation extends Body {
id_Class : one Class,
cmethodInvoked: one Method
}{
(this.@cmethodInvoked in (this.@id_Class).methods) || (this.@cmethodInvoked in ((this.@id_Class).^extend).methods && (this.@cmethodInvoked).acc != private_)
}
// return x;
// return this.x;
// return super.x;
sig FieldInvocation extends Body {
id_fieldInvoked : one Field,
qField: lone Qualifier
}
// return new A().x;
sig ConstructorFieldInvocation extends Body {
id_cf : one Class,
cfieldInvoked: one Field
}{
(this.@cfieldInvoked in (this.@id_cf).fields) || ( this.@cfieldInvoked in ((this.@id_cf).^extend).fields && (this.@cfieldInvoked).acc != private_)
}
在 Java 语言中,如果该方法不是私有方法,我们只能调用类内部的方法(通过该类的实例化)。我试图通过以下签名在我的合金模型中表示此限制:
sig ConstructorMethodInvocation extends Body {
id_Class : one Class,
cmethodInvoked: one Method
}{
(this.@cmethodInvoked in (this.@id_Class).methods || this.@cmethodInvoked in ((this.@id_Class).^extend).methods && (this.@cmethodInvoked).acc != private_)
因此,alloy 中的 ConstructorMethodInvocation 签名试图表示 java 中的构造,如 new A().x()。另外,方法 x() 只有在它不是类 A 的私有方法时才能被调用。所以,为了避免调用类 id_Class 的私有方法,我设置了以下限制(在 ConstructorMethodInvocation 签名中):
(this.@cmethodInvoked in (this.@id_Class).methods || this.@cmethodInvoked in ((this.@id_Class).^extend).methods && (this.@cmethodInvoked).acc != private_)
然而,尽管有这个限制,求解器仍坚持生成实例(用于 ConstructorMethodInvocation),其中 cmethodInvoked 是 id_Class 的私有方法。同样的情况也发生在 ConstructorFieldInvocation 上。
有人看到我做错了吗?