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 +} + + +```