module addressBook
sig Name, Addr {}
sig Book {addr: Name -> Addr}

fun add (b, b': Book, n: Name, a: Addr) {b'.addr = b.addr + n->a}
fun del (b, b': Book, n: Name) {b'.addr = b.addr - n->Addr}
fun lookup (b: Book, n: Name): set Addr {result = b.addr[n]}

assert delUndoesAdd {all b,b',b": Book, n: Name, a: Addr |
	add (b,b',n,a) and del (b',b",n) => b.addr = b".addr }

assert addIdempotent {all b,b',b": Book, n: Name, a: Addr |
	add (b,b',n,a) and add (b',b",n,a) => b'.addr = b".addr }
assert addLocal {all b,b': Book, n,n': Name, a: Addr |
	add (b,b',n,a) and n != n' => lookup (b,n') = lookup (b',n') }

check delUndoesAdd for 3
check addIdempotent for 3
check addLocal for 3 but 2 Book