1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
package java.util;
class HashMapIntegerLong {
//@ model mappings hashmap_model;
/*@ ensures this.hashmap_model == empty_mappings();
@*/
HashMapIntegerLong();
/*@ requires x != null;
@ assigns hashmap_model;
@ ensures
@ this.hashmap_model == update(\old(this.hashmap_model),x,y);
@*/
void put(Integer x, Long y);
/*@ requires x != null;
@ assigns \nothing;
@ behavior key_found:
@ ensures \result != null ==>
@ containsKey(this.hashmap_model,x) &&
@ \result == access(this.hashmap_model,x) ;
@ behavior null_found:
@ assumes containsKey(this.hashmap_model,x);
@ ensures access(this.hashmap_model,x) == null ;
@
@*/
Long get(Integer x);
}
|
