diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/hashmap/Hashmap.Properties.fsti | 29 |
1 files changed, 23 insertions, 6 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fsti b/tests/hashmap/Hashmap.Properties.fsti index 7728bb81..756ae687 100644 --- a/tests/hashmap/Hashmap.Properties.fsti +++ b/tests/hashmap/Hashmap.Properties.fsti @@ -108,10 +108,11 @@ val hash_map_len_fwd_lem (#t : Type0) (self : hash_map_t t) : (**** [insert'fwd_back] *) -/// The backward function for [insert] (note it is named "...'fwd_back" because -/// the forward function doesn't return anything, and is was thus filtered - in a +/// The backward function for [insert] (note it is named "...insert'fwd_back" because +/// the forward function doesn't return anything, and was thus filtered - in a /// sense the effect of applying the forward function then the backward function is -/// entirely given by the backward function alone). +/// entirely encompassed by the effect of the backward function alone). +/// /// [insert'fwd_back] simply inserts a binding. val hash_map_insert_fwd_back_lem (#t : Type0) (self : hash_map_t t) (key : usize) (value : t) : @@ -142,7 +143,7 @@ val hash_map_insert_fwd_back_lem (**** [contains_key] *) -/// [contains_key'fwd] can't fail and return `true` if and only if there is +/// [contains_key'fwd] can't fail and returns `true` if and only if there is /// a binding for key [key] val hash_map_contains_key_fwd_lem (#t : Type0) (self : hash_map_t t) (key : usize) : @@ -168,7 +169,12 @@ val hash_map_get_fwd_lem (**** [get_mut'fwd] *) -/// [get_mut'fwd] returns (mutable borrows to) the binding for key [key]. +/// [get_mut'fwd] returns (a mutable borrow to) the binding for key [key]. +/// +/// The *forward* function models the action of getting a borrow to an element +/// in Rust, which gives the possibility of modifying this element in place. Then, +/// upon ending the borrow, the effect of the modification is modelled in the +/// translation through a call to the backward function. val hash_map_get_mut_fwd_lem (#t : Type0) (self : hash_map_t t) (key : usize) : Lemma @@ -193,6 +199,15 @@ val hash_map_get_mut_back_lem hash_map_t_inv hm /\ // A call to the backward function must follow a call to the forward // function, whose success gives us that there is a binding for the key. + // In the case of *forward* functions, "success" has to be understood as + // the absence of panics. When translating code from Rust to pure lambda + // calculus, we have the property that the generated calls to the backward + // functions can't fail (because their are preceded by calls to forward + // functions, which must then have succeeded before): for a backward function, + // "failure" is to be understood as the semantics getting stuck. + // This is of course true unless we filtered the call to the forward function + // because its effect is encompassed by the backward function, as with + // [hash_map_clear_fwd_back]). Some? (find_s hm key))) (ensures ( match hash_map_get_mut_back t hm key ret with @@ -210,7 +225,9 @@ val hash_map_get_mut_back_lem (**** [remove'fwd] *) /// [remove'fwd] returns the (optional) element which has been removed from the map -/// (the rust function *moves* it out of the map). +/// (the rust function *moves* it out of the map). Note that the effect of the update +/// on the map is modelles through the call to [remove'back] ([remove] takes a +/// mutable borrow to the hash map as parameter). val hash_map_remove_fwd_lem (#t : Type0) (self : hash_map_t t) (key : usize) : Lemma |