vault backup: 2023-10-23 15:14:38

4a1s/MFES/PL - Aula 5.md

@@ -0,0 +1,49 @@
+```c
+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
+  	all x: Node | x->x not in 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
+  	
+  	// for all buckets 
+  
+}
+
+```