通过传递闭包以递归方式使用Alloy函数 [英] Using Alloy functions in a recursive way through transitive closures

问题描述

我在Alloy中做一个模型来表示Java语言的一个子集。下面我们有这个模型的一些元素：

  sig方法{
 id：one MethodId，
 param ：lone Type，
 return：one类型，
 acc：lone辅助功能，
b：one Block 
} 
 
抽象sig表达式{} 
抽象sig StatementExpression扩展表达式{} 
 
 sig MethodInvocation扩展StatementExpression {
 pExp：lone PrimaryExpression，
 id_methodInvoked：one方法，
 param：lone类型
 
 
 sig块{
语句：seq StatementExpression 
} 
 
 pred noRecursiveMethodInvocationCall [] {
 no m：Method | m in ^ getMethodInvokedInsideBody [m] 
} 
 
 fun getMethodInvokedInsideBody [m：Method]：Method {
（univ。（mbstatements））。id_methodInvoked 
} b $ b 

问题是，Block必须是StatementExpression的序列，同时递归调用方法应避免。

当我尝试生成相应的实例时，我得到以下错误类型：

 。 
无法解析名称;可能不正确
 function /谓词调用;也许你used（）当你
应该使用[] 
 
这不能是一个正确的调用fun 
 genericLawsMetaModel / javametamodel_withfield_final / getMethodInvokedInsideBody。 
参数是
 m：
 {genericLawsMetaModel / javametamodel_withfield_final / Method} 
因此参数不能为空。 
 

仍然关于这个问题，我也试图改变谓词noRecursiveMethodInvocationCall的定义（从而消除了上述函数）：

  pred noRecursiveMethodInvocationCall [] {
 no m：Method | m in ^（（univ。（mbstatements））。id_methodInvoked）
} 
  

，将发生新的类型错误：

  ^只能与二元关系一起使用。 
相反，其可能的类型是：
 {genericLawsMetaModel / javametamodel_withfield_final / Method} 
  


$ b b

任何线索？我只想避免递归调用相同的方法。
提前感谢，

解决方案

您误用了传递闭包算子 ^ 。
后者仅适用于二元关系，而不适用于函数。

因此我将MethodInvokedInsideBody声明为Method的一个字段，并使用传递闭包

希望它有帮助：）

EDIT： >

下面是一个示例，说明如何使用传递闭包操作符来实现您想要实现的目标：

  sig方法{
 id：one MethodId，
 param：lone Type，
 return：one Type，
 acc：lone辅助功能，
b：one Block 
 methodInvokedInsideBody：set方法
} 
 
 pred noRecursiveMethodInvocationCall {
 no m：Method | m in m。^ methodsInvokedInsideBody 
} 
  

I am doing a model in Alloy to represent a subset of Java language. Below we have some elements of this model:

sig Method {
    id : one MethodId,
    param: lone Type,
    return: one Type,
    acc: lone Accessibility,    
    b: one Block
}

abstract sig Expression {}
abstract sig StatementExpression extends Expression {}

sig MethodInvocation extends StatementExpression{
    pExp: lone PrimaryExpression, 
    id_methodInvoked: one Method,
    param: lone Type
}

sig Block {
    statements: seq StatementExpression
}

pred noRecursiveMethodInvocationCall [] {
    no m:Method | m in ^getMethodInvokedInsideBody[m]
}

fun getMethodInvokedInsideBody [m: Method] : Method {
      (univ.(m.b.statements)).id_methodInvoked
}

The problem is that Block has to be a sequence of StatementExpression at the same time that recursive calls to the same method should be avoided. Thus, I thought in the solution above.

When i try to generate the corresponding instances i get the following error type:

.
Name cannot be resolved; possible incorrect
function/predicate call; perhaps you used ( ) when you
should have used [ ]

This cannot be a correct call to fun
genericLawsMetaModel/javametamodel_withfield_final/getMethodInvokedInsideBody.
The parameters are
m:
{genericLawsMetaModel/javametamodel_withfield_final/Method}
so the arguments cannot be empty.

Still regarding this question, i also tried changing the definition for the predicate noRecursiveMethodInvocationCall (thus eliminating the mentioned function):

pred noRecursiveMethodInvocationCall [] {
    no m:Method | m in ^( (univ.(m.b.statements)).id_methodInvoked )
}

However, a new type error occurs:

^ can be used only with a binary relation.
Instead, its possible type(s) are:
{genericLawsMetaModel/javametamodel_withfield_final/Method}

Any clue? I just want to avoid recursive calls to the same method. Thanks in advance,

解决方案

You are misusing the transitive closure operator ^. This latter applies on binary relations solely, not on functions.

I would thus declare MethodInvokedInsideBody as a field of the Method and use transitive closure on it the way you did.

Hope it helps :)

EDIT:

Here is an example of how the transitive closure operator can be used in order to achieve what you want to achieve:

sig Method {
    id : one MethodId,
    param: lone Type,
    return: one Type,
    acc: lone Accessibility,    
    b: one Block
    methodsInvokedInsideBody: set Method
}

pred noRecursiveMethodInvocationCall{
    no m:Method | m in m.^methodsInvokedInsideBody
}

这篇关于通过传递闭包以递归方式使用Alloy函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！