Как получить ограничение множественности «один» с помощью языка Alloy Kernel?

Я читал Приложение C: Семантика ядра книги Software Abstraction (автор Дэниел Джексон, второе издание, очень приятно читать, кстати!) и обнаружил, что немного застрял в понимании того, как получить ограничение множественности one, используя другие конструкции ядра.

Я понимаю, что no можно получить, используя expr = none, а some можно вывести, используя отрицание предыдущего правила, но я не понимаю, как выразить ограничение one (и, следовательно, lone), используя только конструкции ядра (или производные).

Я, вероятно, упускаю что-то очевидное, но я этого не вижу :)


alloy
person Jouke Stoel    schedule 19.06.2020    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Вот как я бы выразил one expr

//there is some expr
not (expr = none)
//and all expr should be one and the same because there's only one expr. 
all x1,x2: expr | x1=x2
person Loïc Gammaitoni    schedule 22.06.2020
comment
Ницца! Спасибо! Это действительно хороший способ выразить это. Интересно, есть ли еще способы сделать это. - person Jouke Stoel; 22.06.2020
comment
ммм, может быть, мне также было бы интересно увидеть другие решения ^^ - person Loïc Gammaitoni; 22.06.2020

arrow_upward
1
arrow_downward

Вы можете определить one следующим образом:

one e iff
not all x: e | not x = x // e is non-empty
and
all x: e | all x': e | x = x' // e has no more than one member

Обратите внимание, что языка ядра недостаточно для выражения количественных оценок более высокого порядка (которые поддерживаются Alloy*, но не очень эффективно самим Alloy). Таким образом, квантификатор дает нам понятие синглтона.

Даниэль

person Daniel Jackson    schedule 23.06.2020
comment
Уважаемый Даниил, извините, что пропустил ваш ответ раньше! Когда я сравниваю оба ответа, вы расходитесь в определении no expr, переписывая его в количественную версию not all x:e | not x = x, но другое ограничение похоже на то, которое предлагает Лоик. Спасибо за ваше понимание! - person Jouke Stoel; 07.07.2020