vault backup: 2023-11-10 12:11:37
This commit is contained in:
parent
b3a6cdf38c
commit
4f479bc45b
1 changed files with 20 additions and 7 deletions
|
@ -41,19 +41,32 @@ sig Hash {}
|
|||
pred insert[n : Node] {
|
||||
always n in ( Bucket.head + Bucket.head.prox)
|
||||
always n in Bucket.head or n in Node.prox
|
||||
|
||||
//if hash empty -> node to head of bucket
|
||||
|
||||
//if hash empty -> node to head of bucket
|
||||
n.key.hash not in Hash implies
|
||||
(
|
||||
lone b:Bucket | b.head = none implies b.head' = n
|
||||
)
|
||||
//if hash empty -> bucket of desired hash, add to next
|
||||
n.key.hash in Hash implies
|
||||
(
|
||||
)
|
||||
//if hash empty -> bucket of desired hash, add to next
|
||||
n.key.hash in Hash implies
|
||||
(
|
||||
lone b: Bucket | b.head.key.hash = n.key.hash | b.head.*prox = n
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
|
||||
pred insert[n : Node] {
|
||||
//nodes always in the head or linked to prox
|
||||
//always n in ( Bucket.head + Bucket.head.prox)
|
||||
always{
|
||||
n in Bucket.head
|
||||
}
|
||||
|
||||
historically n.key.hash not in Hash
|
||||
lone b:Bucket | b.head = none implies b.head' = n
|
||||
|
||||
|
||||
}
|
||||
|
||||
|
||||
```
|
||||
|
|
Loading…
Add table
Reference in a new issue