понимание ключевого слова this в Alloy

К чему относится ключевое слово this в следующем коде из раздела 4.7.2 книги Alloy?

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.


alloy
person qartal    schedule 01.01.2015    source источник

Ответы (1)


arrow_upward
7
arrow_downward

Раздел 4.5.2 книги Software Abstractions описывает (среди прочего) то, что он называет соглашением «получателя», то есть синтаксическим сокращением написания функций и предикатов как

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 в Alloy. Вот опрос. Ключевое слово this можно использовать в следующих ситуациях:

  • В объявлениях и фактах подписи this действует как переменная, неявно связанная с каждым экземпляром подписи. Таким образом, объявление формы

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

    эквивалентно

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

  • В объявлениях и фактах подписи каждая ссылка на поле f, объявленное или унаследованное подписью, неявно расширяется до this.f, где this неявно связывается, как описано выше, если ссылка не имеет префикса @. Пример в конце 4.2.4 иллюстрирует семантику.

  • В телах объявлений функций и предикатов, объявленных с использованием соглашения «получатель», ключевое слово this действует как переменная, неявно связанная с первым аргументом функции или предиката. Пример в конце 4.5.2 иллюстрирует это, как и пример, приведенный здесь OP.

    Соглашение о «получателе» определено в разделе B.7.5 справочника по языку.

На все это указывает запись this в указателе Software Abstractions; для получения дополнительной информации прочитайте соответствующие отрывки.

person C. M. Sperberg-McQueen    schedule 01.01.2015