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

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

Browse source
This commit is contained in:
Alice 2023-10-23 20:08:40 +01:00
parent 64958b9fd5
commit 7cd1ca9a1f
1 changed files with 11 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -44,7 +44,14 @@ pred Invs {
//ALTERNATIVELY //ALTERNATIVELY
//no node links to nodes associated with a different hash //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
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
//MAY BE WORNG STUFF //MAY BE WORNG STUFF
@ -54,7 +61,9 @@ pred Invs {
//the prox node of another node may be empty //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, y : Node | x.prox = y or not x.prox = y
//all x : Node | x.prox.key != x.key //the sequence of nodes associated with the same hash should not loop
//all x : Node | x.prox.key != x.key
//WORNG STUFF //WORNG STUFF