2.1 KiB
2.1 KiB
sig Bucket {
head : lone Node
}
sig Node {
key : one Key,
prox : lone Node
}
sig Key {
hash : one Hash
}
sig Hash {}
pred Invs {
// Specify the properties that characterize
// hash tables using closed addressing (separate
// chaining) for collision resolution.
// The points you will get is proportional to the
// number of correct properties. To check how many
// points you have so far you can use the different
// commands. For example, if check Three is correct
// you will have at least 3 points.
// The maximum is 5 points.
// Be careful to not overspecify!
// If you specify a property that is not valid in
// these hash tables you get 0 points,
// even if you have some correct properties.
// To check if you are not overspecifying you can use
// command NoOverspecification. If you have an invalid
// property this command will return a valid hash table
// that you specification is not accepting.
//no node links to itself and its children don't link to it (no loops)
all x: Node | x not in x.^prox
//ALTERNATIVELY (INCOMPLETE)
//all x: Node | x not in x.prox
//all x, y, z:Node, w : Key | (x.key = w and y.key = w and z.key = w and x.prox = z) implies y.prox!=z
//for all nodes sequentially linked, they must have the same hash
all x, y: Node | (x.prox = y) implies x.key.hash = y.key.hash
//ALTERNATIVELY
//all x, y: Node | x.key.hash != y.key.hash implies (x.prox != y and y.prox != x)
//keys are unique to a single node
all k: Key | one x: Node | x.key = k
//heads are unique to a single bucket (UNNECESSARY)
all x: Bucket | lone x.head
//nodes must be prox to another node or be the head of a bucket
all x: Node | (x in Bucket.head) or (x in Node.prox)
//diffenrent buckets must have different heads
all x, y: Bucket, z : Node | x != y and x.head = z implies y.head!=z
//keys must have a hash
all x: Key | some y: Hash | x.hash = y
//nodes(heads) associated to different buckets, must differ in hash
all x, y: Bucket | (x != y and x.head != none and y.head != none ) implies x.head.key.hash != y.head.key.hash
}