From 45cfc4c296b4c67ba2384ed10e72821f6a2c3f47 Mon Sep 17 00:00:00 2001 From: Alice Date: Mon, 23 Oct 2023 20:58:40 +0100 Subject: [PATCH] vault backup: 2023-10-23 20:58:40 --- 4a1s/MFES/PL - Aula 5.md | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/4a1s/MFES/PL - Aula 5.md b/4a1s/MFES/PL - Aula 5.md index ba43366..db1eb5a 100644 --- a/4a1s/MFES/PL - Aula 5.md +++ b/4a1s/MFES/PL - Aula 5.md @@ -44,7 +44,7 @@ pred Invs { 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) + //all x, y: Node | x.key.hash != y.key.hash implies (x.prox != y and y.prox != x) //a node with the same hash as two others in the same hash cannot be prox of them two @@ -52,7 +52,17 @@ pred Invs { - + //heads are unique to a single bucket + all x: Bucket | lone x.head + + //nodes must be prox to another node or be the head of a bucket + all x: Node | (x in Bucket.head) or (x in Node.prox) + + //diffenrent buckets must have different heads + all x, y: Bucket, z : Node | x != y and x.head = z implies y.head!=z + + //keys must have a hash + all x: Key | some y: Hash | x.hash = y