CODEWITHSUNDEEP
alloy
hooleyhoop
hooleyhoop

Reputation: 9198

How to read sequenced declarations?

In appendix B: Alloy Language Reference of Software Abstractions it is stated that

all x: X, y: Y | F

is short for

all x: X | all y: Y | F

but

one x: X, y: Y | F

is not short for

one x: X | one y: Y | F

I can't quite see clearly what is going on here and it occurs to me i am perhaps not reading this correctly at all..

my attempt would be "this is true if there is one instance, comprised of one x from X and one y from Y for which F is true".

Upvotes: 1

Views: 93

Answers (1)

Grayswandyr
Grayswandyr

Reputation: 542

Intuitively, one x: X, y: Y | F means "there is exactly one pair (x,y) in XxY s.t. F", while one x: X | one y: Y | F means "there is exactly one x in X s.t: there is exactly one y in Y s.t. F". In the latter case, the unique y s.t. F may depend on the given x.

To see what happens formally, you could translate one in terms of all and some; and then recast your example this way.

Upvotes: 2

Related Questions