理解Alloy中的'this'关键字

Question

在Alloy book的4.7.2节的下面的代码中,this关键字引用了什么？

module library/list [t]
sig List {}
sig NonEmptyList extends List {next: List, element: t} 

...

fun List.first : t {this.element} 
fun List.rest : List {this.next} 
fun List.addFront (e: t): List {
    {p: List | p.next = this and p.element = e} 
}

如果您在Alloy中详细说明这种用法,我将不胜感激.

Answer 1

软件抽象的 4.5.2节描述了(除其他事项外)它所谓的"接收器"约定,即将函数和谓词写成的语法简写

fun X.f[y : Y, ...] { ... this ... }

代替

fun f[x : X, y : Y, ...] { ... x ... }

那就是声明

fun List.first : t {this.element} 

相当于(和速记/句法糖)

fun first[x : List] : t {x.element} 

对于你给出的其他例子,同样如此.如果我们说长形式,那么平行将会更强

fun first[this : List] : t {this.element} 

虽然这是一个有用的例子,但它不合法: this是一个关键字,不能用作普通的变量名.

您要求对thisAlloy 中的用法进行"详细说明" .这是一项调查.该关键字this可用于以下情况:

• 在声明和签名事实中,this充当隐式绑定到签名的每个实例的变量.所以表格的声明

  sig Foo { ... } { copacetic[this] }
  

  相当于

  sig Foo { ... }
  fact { all f : Foo | copacetic[f] }
  

• 在声明和签名事实中,除非引用带有前缀,否则对f签名声明或继承的字段的每个引用都会隐式扩展为this.f,this如上所述隐式绑定@.4.2.4结尾的例子说明了语义.

• 在使用'receiver'约定声明的函数和谓词的声明体中,关键字this充当隐式绑定到函数或谓词的第一个参数的变量.4.5.2结尾处的示例说明了这一点,OP中引用的示例也是如此.

  "接收者"约定在语言参考的B.7.5节中定义.

所有这些都是从软件抽象this索引中的条目中指出的; 有关更多信息,请阅读相关段落.