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

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

Browse source
This commit is contained in:
Alice 2023-10-23 20:38:40 +01:00
parent ec8d5f1ba9
commit 380ec14507
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -36,17 +36,19 @@ pred Invs {
// that you specification is not accepting. // that you specification is not accepting.
//no node links to itself and its children don't link to it //no node links to itself and its children don't link to it (no loops)
all x: Node | x not in x.^prox all x: Node | x not in x.^prox
//for all nodes sequentially linked, they must have the same hash //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 all x, y: Node | (x.prox = y) implies x.key.hash = y.key.hash
//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 //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 //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