diff --git a/4a1s/MFES/PL - Aula 5.md b/4a1s/MFES/PL - Aula 5.md index 7e8d280..9565f97 100644 --- a/4a1s/MFES/PL - Aula 5.md +++ b/4a1s/MFES/PL - Aula 5.md @@ -44,7 +44,14 @@ pred Invs { //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 + + + + + //MAY BE WORNG STUFF @@ -54,7 +61,9 @@ 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 + //the sequence of nodes associated with the same hash should not loop + //all x : Node | x.prox.key != x.key + //WORNG STUFF