From 64958b9fd561c33e7b8ca3c714aa97d9125e8132 Mon Sep 17 00:00:00 2001 From: Alice Date: Mon, 23 Oct 2023 19:58:40 +0100 Subject: [PATCH] vault backup: 2023-10-23 19:58:40 --- 4a1s/MFES/PL - Aula 5.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/4a1s/MFES/PL - Aula 5.md b/4a1s/MFES/PL - Aula 5.md index 41d3174..7e8d280 100644 --- a/4a1s/MFES/PL - Aula 5.md +++ b/4a1s/MFES/PL - Aula 5.md @@ -41,7 +41,7 @@ pred Invs { //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) @@ -54,9 +54,15 @@ pred Invs { //the prox node of another node may be empty all x: Node, y : Node | x.prox = y or not x.prox = y +//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 } ``` \ No newline at end of file