0

我正在为 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 上。

有人看到我做错了吗?

4

1 回答 1

1

这是因为您在ConstructorMethodInvocationsig 的附加事实中放错了括号:现在的方式是,您有一个顶级析取,它允许 (cmethodInvokedid_Class.methods) 或 (它在id_Class.^extend.methods而不是私有) 的实例。如果您将附加的事实块更改为

{
   this.@cmethodInvoked in this.@id_Class.*extend.methods 
   this.@cmethodInvoked.acc != private_
}

您将获得预期的行为(星号运算符 ( *) 是反射传递闭包,它的含义与您打算编写的原始析取基本相同;您仍然可以使用旧约束并修复括号)。

为了检查不存在ConstructorMethodInvocation该方法是私有的任何实例,我执行了

check {
  no c: ConstructorMethodInvocation {
    c.cmethodInvoked.acc = private_
  }
}

没有找到反例。

于 2013-09-25T19:50:12.277 回答