summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-02-14 11:53:39 +0100
committerSon Ho2022-02-14 11:53:39 +0100
commiteda5faea35e1032c1735768adc57f2be4d93910f (patch)
tree406ad3e4fdf49350380de94f6233c2783ff78f04
parentc9fd7cd50fd8ed08808bb3a682baddd525c4c448 (diff)
Make minor modifications
Diffstat (limited to '')
-rw-r--r--tests/hashmap/Hashmap.Properties.fsti7
1 files changed, 4 insertions, 3 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fsti b/tests/hashmap/Hashmap.Properties.fsti
index 80c0de06..7728bb81 100644
--- a/tests/hashmap/Hashmap.Properties.fsti
+++ b/tests/hashmap/Hashmap.Properties.fsti
@@ -42,7 +42,8 @@ val hash_map_not_overloaded_lem (#t : Type0) (hm : hash_map_t t) :
// if there are more entries than a given fraction of the number of slots,
// we resize the slots vector to limit the hash collisions
let (dividend, divisor) = hm.hash_map_max_load_factor in
- // This postcondition won't typecheck if we don't reveal that divisor > 0
+ // technicality: this postcondition won't typecheck if we don't reveal
+ // that divisor > 0 (because of the division)
divisor > 0 /\
begin
// The max load, computed as a fraction of the capacity
@@ -53,8 +54,8 @@ val hash_map_not_overloaded_lem (#t : Type0) (hm : hash_map_t t) :
// We prove that:
// - either the number of entries is <= than the max load threshold
len <= max_load
- // - or we couldn't resize the map, because then it would overflow
- // (note that we always multiply the number of slots by 2)
+ // - or we couldn't resize the map, because then the arithmetic computations
+ // would overflow (note that we always multiply the number of slots by 2)
|| 2* capacity * dividend > usize_max
end))