gpt4 book ai didi

java - 生成明显不一致的合金实例

转载 作者:行者123 更新时间:2023-12-01 14:04:41 25 4
gpt4 key购买 nike

我正在为 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语言中,如果某个方法不是私有(private)方法,我们只能调用类内部的方法(通过该类的实例化)。我尝试通过以下签名在我的合金模型中表示此限制:

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_)

因此,合金中的 ConstructorMethodInitation 签名尝试表示 Java 中的构造,如 new A().x()。另外,方法 x() 只有在不是类 A 的私有(private)方法时才能被调用。因此,我添加了以下限制(在 ConstructorMethodInitation 签名中)以避免调用类 id_Class 的私有(private)方法:

(this.@cmethodInvoked in (this.@id_Class).methods || this.@cmethodInvoked in ((this.@id_Class).^extend).methods && (this.@cmethodInvoked).acc != private_)

但是,尽管有此限制,求解器仍坚持生成实例(对于 ConstructorMethodInitation),其中 cmethodInvoked 是 id_Class 的私有(private)方法。同样的情况也发生在 ConstructorFieldInitation 上。

有人看出我做错了什么吗?

最佳答案

这是因为您在 ConstructorMethodInitation 信号的附加事实中放错了括号:按照现在的方式,您有一个顶级析取,它允许实例 (cmethodInvoked) > 在 id_Class.methods 中)或者(在 id_Class.^extend.methods 中并且不是私有(private)的)。如果您将附加事实 block 更改为

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

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

为了检查是否不存在任何方法为私有(private)的 ConstructorMethodInitation 实例,我执行了

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

没有发现反例。

关于java - 生成明显不一致的合金实例,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/19007092/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com