my_digital_garden/4a1s/MFES/PL - Aula 5.md

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


  	//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
  	//no node links to nodes associated with a different hash
  	//all x, y: Node | x.key.hash != y.key.hash implies (x.prox != y and y.prox != x)


  	//a node with the same hash as two others in the same hash cannot be prox of them two
  	//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



    //heads are unique to a single bucket
  	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



  	//MAY BE WORNG STUFF
  	//the head of a bucket may be empty
  	all x: Bucket, y : Node | x.head = y or not x.head = y
  
  	//the prox node of another node may be empty
  	all x: Node, y : Node | x.prox = y or not x.prox = y

  	//the sequence of nodes associated with the same hash should not loop
  	//all x : Node | x.prox.key != x.key



  	//WORNG STUFF
  	//buckets may only have one head exclusive to it
  	all x, y : Bucket| all z : Node | x.head = z implies y.head != z
  	
  	//all buckets have a unique hash
  	all x, y: Bucket | (x.head != none and y.head != none) implies x.head.key.hash != y.head.key.hash 
}