lists 1

One of my research topics may involve Alloy in its role as a language for developing software. The problem is, I don't know Alloy quite well enough to use it in anger yet. That's something I must fix.

I need a nice, simple TODO list-keeping application, and so I'll try modeling it with Alloy. I'll try to verbalize my thinking in real-time, just to show that software isn't written in a vacuum, but is revised and re-revised.

These are the sort of things I'd want in a TODO list manager:

• I should be able to make Items, and going the other way, deleting should be a snap.


• I should be able to assign items to Tags.


• I should be able to easily share my TODO lists with other people.

It's the last requirement that seems interesting to me; I'm not quite sure what I mean by this yet, but it involves some kind of security thing that I'll think about more in a moment. But let me first start modeling the relationships between the items in my imaginary system.

module lists
sig Person {
    tags: set Tag,
    items: set Item
}
sig Tag {}
sig Public, Private extends Tag {}
sig Item {
    tags: set Tag
}
run {}

I'm thinking of a design like delicious: a Person manages their TODO Items by tagging them. I'll keep two special tags called Public and Private, which I'll plan to use to restrict views by other people. Maybe it's premature to think about this...

Oh, I do want to say that the tags that are associated with a person are the ones used in that person's items: at the moment, my software model leaves that unconstrained. Let me fix that and revise the definition of a Person.

sig Person {
    tags: set Tag,
    items: set Item
} {
    tags = items.tags
}

At this point, I can ask Alloy: what would a possible situation of my model look like, by executing and showing a model. Here's one sample visualization that the tool's giving me.

Ok, but I haven't yet done anything about privacy yet; I need to model the items that a person might be looking at the moment. Let me extend a Person to also include the items that they're currently looking at, and also assign an "owner" to each Item.

module lists
sig Person {
    tags: set Tag,
    items: set Item,
    viewing: set Item
} {
    tags = items.tags
}
sig Tag {}
sig Public, Private extends Tag {}
sig Item {
    tags: set Tag,
    owner: one Person
}
run {}

Ok, so Items know who own them, so I should be able to write an expression capturing a notion of privacy. It might not be completely right, but let me see what things look like.

pred respectsPrivacy(p : Person) {
    all i : p.viewing | permit[p, i]
}
pred permit(p : Person, i : Item) {
    p = i.owner || Public in i.tags
}

Cool. Hmm, when I visualize this, though, the diagram's a little cluttered. And on second thought, I don't really need to have a Person keep track of their items's tags explicitely: that's easily computable as a function.

sig Person {
    items: set Item,
    viewing: set Item
}
// Returns the tags used by a Person
fun personalTags(p : Person) : set Tag {
    p.items.tags
}

Ok, let me visualize again, with a more interesting scenario.

pred show {
    all p : Person | respectsPrivacy[p]
    #Person > 1
    some p : Person | some i : Item {
        permit[p, i] && i.owner != p
    }
}
run show

Wait a minute, the diagram doesn't look right at all. Why does Person0 see Item0: she doesn't own it. Ooooh... I didn't tell my design that a Person's items must be owned by them. Ooops. I want to prevent panhandling.

Actually, let me just simplify the model so that this issue doesn't even happen. Just as I treated the personal tags as a function, I'll just make a personalItems function to compute whenever I need it.

// Returns a set of the items owned by this person.
fun personalItems(p : Person) : set Item {
    { i : Item | i.owner = p }
}

Here's my revised model so far.

module lists

sig Person {
    viewing: set Item
} 

// Returns a set of the items owned by this person.
fun personalItems(p : Person) : set Item {
    { i : Item | i.owner = p }
}

// Returns the tags used by a Person
fun personalTags(p : Person) : set Tag {
    p.personalItems.tags
}

sig Tag {}
sig Public, Private extends Tag {}

sig Item {
    tags: set Tag,
    owner: one Person
}

pred respectsPrivacy(p : Person) {
    all i : p.viewing | permit[p, i]
}

pred permit(p : Person, i : Item) {
    p = i.owner || Public in i.tags
}

pred show {
    all p : Person | respectsPrivacy[p]
    #Person > 1
    some p : Person | some i : Item {
        permit[p, i] && i.owner != p
    }
}

assert privateReallyMeansPrivate {
    all i : Item | all p : Person {
        (Private in i.tags && permit[p, i]) implies (i.owner = p)
    }
}

run show
check privateReallyMeansPrivate

I also added an assertion making sure that "private" really means private. There are plenty of counterexamples! It fails because my definition for permit() currently only cares about Public at the moment, and it's very easy for an Item to get tagged both with the Public and Private tag at once.

This is pretty cool stuff! To be able to talk about this software's design even without touching a single hashtable or SQL statement is really nice, and I'm already hitting core issues like handling privacy. But since the post is getting a bit long, I'll stop for now and continue this when I get back to Massachusetts tomorrow.