Alice/my_digital_garden
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

vault backup: 2023-10-23 21:08:40

Browse source
This commit is contained in:
Alice 2023-10-23 21:08:40 +01:00
parent 45cfc4c296
commit cc7a937675
1 changed files with 5 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
4a1s/MFES/PL - Aula 5.md
View file

@ -38,19 +38,18 @@ pred Invs {
//no node links to itself and its children don't link to it (no loops)
all x: Node | x not in x.^prox
//ALTERNATIVELY (INCOMPLETE)
//all x: Node | x not in x.prox
//all x, y, z:Node, w : Key | (x.key = w and y.key = w and z.key = w and x.prox = z) implies y.prox!=z
//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)
//a node with the same hash as two others in the same hash cannot be prox of them two
//all x, y, z:Node, w : Key | (x.key = w and y.key = w and z.key = w and x.prox = z) implies y.prox!=z
//keys are unique to a single node
all k: Key | one x: Node | x.key = k
//heads are unique to a single bucket
all x: Bucket | lone x.head
@ -64,26 +63,6 @@ pred Invs {
//keys must have a hash
all x: Key | some y: Hash | x.hash = y
//MAY BE WORNG STUFF
//the head of a bucket may be empty
all x: Bucket, y : Node | x.head = y or not x.head = y
//the prox node of another node may be empty
all x: Node, y : Node | x.prox = y or not x.prox = y
//the sequence of nodes associated with the same hash should not loop
//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
}
```