Tip: pitfalls with using `in` for typechecking

Alloy 6
1

Say you have this:

sig Person {
  pet: lone Animal
}

abstract sig Animal {}
sig Cat, Dog, Bird extends Animal {}

You want to check if alice has a Dog. The obvious thing to do would be

alice.pet in Dog

Be careful! Since pet is lone, it’s possible that alice doesn’t have a pet, in which case alie.pet in Dog is true!

If you actually want to check “alice’s pet is a Dog”, you instead have to write

some alice.pet & Dog

This problem cropped up in a couple of models I’m working on, so this is a PSA about it :slight_smile:

(I had a similar problem with foo.bar = baz.qux when both were empty, I needed some foo.bar & baz.qux instead.)

4 Likes
2

Yes! Note that the claim that S is a subset of T is conventionally written in logic as

all e: univ | e in S implies e in T

which becomes vacuously true when S is empty. This treatment of partial functions and empty sets is one of Alloy’s key innovations, and it avoids the nastiness of undefined values that complicated many languages before Alloy.

For those not familiar with that whole rats nest, consider that the formula

some p: Person | p.dog = Rex

becomes undefined in most standard logics if there is any person who doesn’t have a dog, even if Rex is Alice’s dog!

A downside of this is indeed that you need to sometimes strengthen a constraint if you don’t want to subsume the empty case. In an early version of Alloy there was a special operator that you could use to say S is a non-empty subset of T, but I can’t remember what it was. It was a bad idea anyway :-).

2 Likes
3

Hitting this pitfall already in Exercise 1.d of Structural design with Alloy in Formal Software Design with Alloy 6.

4

Hit this again trying to write a proper temporal model.
Can we maybe have a lint against this? or is it related to any other vacuous stuff? lol

5

Since partial fields (i.e yielding none or set) and joins are so common, you would likely end up with tons of warnings, even when you would have checked beforehand that there’s no risk of vacuousness.