From 022cfa22f761ba479502e76139603266babf8ecc Mon Sep 17 00:00:00 2001
From: Alice <alicevteixeira@gmail.com>
Date: Mon, 6 Nov 2023 12:25:52 +0000
Subject: [PATCH] vault backup: 2023-11-06 12:25:52

---
 4a1s/MFES/PL - Aula 7.md | 36 +++++++++++++++++++++++++++++++++++-
 1 file changed, 35 insertions(+), 1 deletion(-)

diff --git a/4a1s/MFES/PL - Aula 7.md b/4a1s/MFES/PL - Aula 7.md
index 487346c..177dab4 100644
--- a/4a1s/MFES/PL - Aula 7.md	
+++ b/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 
+}
+
+
+```