Множественности в тернарных отношениях

Семантику нижних множеств some и one в троичных отношениях трудно понять. Согласно Software Abstractions (Rev. ed.), стр. 79–80, отношение addr: Book -> (Name -> some Addr) должно быть эквивалентно all b: Book | b.addr in Name -> some Addr (см. также стр. 97). Но что именно означает последняя формула? Мое воображение здесь не работает. Вот почему я провел несколько экспериментов в Alloy Analyzer 4.1.0. Смысл в этой модели:

sig Name, Addr {}
sig Book { addr: Name -> some Addr }
assert implication {
 #Book = 0 or all n: Name | some b: Book, a: Addr | n in b.addr.a
}
check implication

выполняется (контрпример не найден). Итак, если есть какая-то Книга, каждое Имя должно быть зарегистрировано по крайней мере в одной из этих Книг. Недокументированные Адреса разрешены, и без Книг неожиданно появляются недокументированные Имена.

Импликация в следующей модели:

sig Name, Addr {}
sig Book { addr: Name some -> Addr }
assert implication {
  #Book = 0 or all a: Addr | some b: Book | #b.addr.a > 0
}
check implication

снова держит. Это зеркальное отражение предыдущей модели: недокументированные Addrs запрещены, если только нет Book. И нет никаких ограничений в отношении документации имен.

Обе модели можно объединить и сформулировать более лаконично:

sig Name, Addr {}
sig Book { addr1: Name -> some Addr, addr2: Name some -> Addr }
assert implications {
  some Book implies Name in Book.addr1.Addr and Addr in Book.addr2[Name]
}
check implications

Таким образом, если есть какая-либо Книга, все Имена должны участвовать в отношении addr1, а все Адреса должны участвовать в отношении addr2. Множественность one ведет себя одинаково.

Кажется, что Software Abstractions и Analyzer не рассказывают одну и ту же историю о таких конструкциях, как R: A -> (B m -> n C) в отношении ограничений нижней границы, но я мог что-то упустить. Обнаруженные мной следствия оказались не такими, как я ожидал, и могут быть и другие странные следствия, которые я еще не обнаружил. Я все больше и больше чувствую, что вложенные множественности с нижней границей вообще не имеют смысла. Могу ли я быть прав в этом?


alloy
person Meindert Meindertsma    schedule 19.09.2012    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Первый пример надолго озадачил меня; меня удивило, что ни в одном случае не было неотображенных имен. Однако для чего это стоит, я нахожу на p. 78 первого издания утверждение о том, что «кратности — это просто сокращение, и их можно заменить стандартными ограничениями; ограничение кратности в

r: A m -> n B

можно записать как

all a: A | n a.r
all b: B | m r.b

Применение первого из этих правил перезаписи к оператору

all b: Book | b.addr in Name -> some Addr

который вы получаете из первой модели примера, мы получаем

all b: Book | all n: Name | some n.(b.addr)

или в прозе "для всех книг b и имен n есть некоторое сопоставление для n в b.addr ", что, по крайней мере, снимает мое первоначальное недоумение. Чтобы разрешить несопоставленные имена, нужно написать либо sig Book { addr: set (Name -> Addr) }, либо (как в более поздних примерах в Whirlwind Tour) sig Book { names: set Name, addr: names -> some Addr}.

У меня немного больше проблем со вторым правилом перезаписи (с участием m). Для Name нет явной кратности (нет m), и я потратил некоторое время, просматривая книгу, чтобы найти спецификацию ограничения кратности по умолчанию для отношений (аналогично one по умолчанию для других полей), и поэкспериментировать с различными способами записи эквивалентных ограничений, прежде чем прийти к выводу, что ограничения множественности по умолчанию нет; вместо этого по умолчанию ограничение множественности нет. Таким образом, второе правило перезаписи, данное на с. 78 не относится к Name -> some Addr; ограничения на множественность нет, и в результате для каждого a в Addr может быть ноль или более экземпляров (b.addr).a< /эм>.

Я предполагаю, что с точки зрения дизайна языка, я думаю, может помочь иметь явное «ограничение множественности по умолчанию» set и разрешать такие операторы, как

all b: Book | all a: Addr | set (b.addr).a
/* currently produces type error */

это означает, что для каждого адреса может быть ноль или более записей в b.addr.

Но я склонен думать, что с таким изменением или без него вы все равно будете правы, говоря, что эффекты some и one в троичных отношениях могут быть трудными для понимания.

person C. M. Sperberg-McQueen    schedule 21.09.2012