Я делаю метамодель в сплаве для подмножества 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_)
Таким образом, сигнатура ConstructorMethodInvocation в сплаве пытается представить конструкцию в java, подобную новой A().x(). Кроме того, метод x() может быть вызван только в том случае, если он не является приватным методом класса A. Итак, я поставил следующее ограничение (внутри подписи ConstructorMethodInvocation), чтобы избежать вызова приватных методов класса id_Class:
(this.@cmethodInvoked in (this.@id_Class).methods || this.@cmethodInvoked in ((this.@id_Class).^extend).methods && (this.@cmethodInvoked).acc != private_)
Однако, несмотря на это ограничение, решатель настаивает на создании экземпляров (для ConstructorMethodInvocation), где cmmethodInvoked — это закрытый метод id_Class. То же самое происходит и с ConstructorFieldInvocation .
Кто-нибудь видит, что я делаю неправильно?
