vault backup: 2023-11-06 12:25:52

4a1s/MFES/PL - Aula 7.md

@@ -1,4 +1,4 @@
-
+https://alloy.readthedocs.io/en/latest/language/signatures.html#relations
 
 >[!note]
 >Node.prox' = Node.prox
@@ -7,3 +7,37 @@ all n:Node | n.prox' = n.prox
 = 
 prox' = prox
 
+```c
+// Recall the hash table Alloy model,
+// now with mutable lists inside the buckets.
+
+sig Bucket {
+	var head : lone Node
+}
+sig Node {
+	key : one Key,
+	var prox : lone Node
+}
+sig Key {
+	hash : one Hash
+}
+sig Hash {}
+
+// Specify the operation of inserting a node
+// in the hash table. The node should be 
+// inserted at the head of a bucket.
+// If the operation only works well when the
+// hash of the new node does not exist in the
+// table you get Two points. If it always 
+// works well you get Five points. Use the
+// respective commands to check how many
+// points you have.
+
+pred insert[n : Node] {
+	some k: Hash
+	//if hash empty -> node to head of bucket
+  	//else 
+}
+
+
+```