alloy - 理解 Alloy 中的 'this' 关键字

Question

在 Alloy 书籍第 4.7.2 节的以下代码中， 是什么意思？这个关键字指的是？

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} 
}

如果您能详细描述，我将不胜感激。这个在合金中的使用。

Answer 1

Software Abstractions 的第 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是关键字，不能用作普通变量名。

您要求对 this 的用法进行“详细描述”在合金中。这是一项调查。关键字this可用于以下情况:

在声明和签名事实中，this充当隐式绑定(bind)到签名的每个实例的变量。所以表格的声明

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

相当于

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

在声明和签名事实中，对字段的每次引用 f由签名声明或继承的隐式扩展为 this.f , 其中 this如上所述隐式绑定(bind)，除非引用以 @ 为前缀. 4.2.4 末尾的示例说明了语义。

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

“接收者”约定在语言引用的 B.7.5 节中定义。

所有这些都指向 this 的条目。在软件抽象索引中；欲了解更多信息，请阅读相关段落。