vault backup: 2023-10-23 19:28:40
This commit is contained in:
parent
8aeb806bf4
commit
bbd2f7db9d
2 changed files with 7 additions and 30 deletions
|
@ -42,7 +42,8 @@ pred Invs {
|
|||
//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
|
||||
|
||||
// for all buckets
|
||||
//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)
|
||||
|
||||
}
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue