значение предиката Alloy в реляционном соединении

Рассмотрим следующий простой вариант примера с адресной книгой.

sig Name, Addr {}
sig Book { addr : Name -> Addr } // no lone on Addr
pred show(b:Book) { some n : Name | #addr[b,n] > 1 }
run show for exactly 2 Book, exactly 2 Addr, exactly 2 Name

В некоторых случаях модели я могу получить следующие результаты в оценщике

all b:Book | show[b]
--> yields false
some b:Book | show[b]
--> yields true
show[Book]
--> yields true

Если бы show было отношением, то можно было бы ожидать получить ответ вроде: {true, false}. Учитывая, что это предикат, возвращается одно логическое значение. Я ожидал, что show[Book] будет сокращением универсального квантифицированного выражения над ним. Вместо этого он, кажется, использует экзистенциальную количественную оценку, чтобы сложить результаты. Кто-нибудь знает, что может быть рациональным для этого, или есть другое объяснение значения show[Book]?


alloy
person user2033286    schedule 01.02.2013    source источник

Ответы (1)


arrow_upward
1
arrow_downward

(Я не уверен, что у меня есть правильные слова для этого, так что потерпите меня, если это кажется нечетким.)

Имейте в виду, что все выражения в Alloy, обозначающие индивидуумов, обозначают наборы индивидуумов, и что в языке нет различия между «индивидуумом X» и «одиночным множеством, членом которого является индивидуум X». ([Позднее добавление:] В более часто используемых терминах: общее правило логики Аллоя состоит в том, что все значения являются отношениями. Бинарные отношения — это наборы пар, n-арные отношения — наборы из n-кортежей, множества — это унарные отношения, а скаляры являются одноэлементными множествами. См. обсуждение в разделе 3.2.2 книги Абстракции программного обеспечения или слайд "Все взаимосвязано" в руководство по Alloy Analyzer 4, написанное Грегом Деннисом и Робом Ситером.)

Учитывая объявление предиката show, которое вы даете, легко ожидать, что аргументом show должен быть одиночный Book — или, точнее, одноэлементный набор Book — и далее ожидать, что если аргумент на самом деле не является одноэлементным набором (как в выражении show[Book] здесь), тогда система заставит его быть одноэлементным набором или интерпретирует его с помощью какой-то неявной экзистенциальной или универсальной квантификации. Но в объявлении pred show(b:Book) ... выражение b:Book просто называет объект b, который будет набором объектов в Книге подписи. (Чтобы потребовать, чтобы b было одноэлементным набором, напишите pred show(one b: Book) ....) Выражение, составляющее тело show, вычисляется для b = Book так же легко, как и для b = Book$0.

Появление экзистенциальной квантификации является следствием того, как определяется оператор точки в основе выражения addr[b,n] (или эквивалентно n.(b.addr)). На самом деле, если вы поэкспериментируете, вы обнаружите, что show[Book] истинно всякий раз, когда есть какое-либо имя для что набор всех книг содержит сопоставление с двумя разными адресами, даже в тех случаях, когда экзистенциальная интерпретация не удалась. Попробуйте добавить это в свою модель, например:

pred hmmmm { show[Book] and no b: Book | show[b] }
run hmmmm for exactly 2 Book, exactly 2 Addr, exactly 2 Name
person C. M. Sperberg-McQueen    schedule 01.02.2013
comment
Благодарю за разъяснение. - person user2033286; 02.02.2013