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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
module M
use int.Int
use ref.Ref
use map.Map
let ghost test_map (ghost x : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
=
x := Map.set !x 0 3
(* Multi-dimensional maps *)
let ghost test_map_multidim1 (ghost x : ref (map int (map int int))) : unit
ensures { !x[0][0] <> !x[1][1] }
=
x := Map.set !x 0 (Map.get !x 1)
let ghost test_map_multidim2 (ghost x : ref (map int (map int int))) : unit
ensures { !x[0][0] <> !x[1][1] }
=
let x0 = Map.get !x 0 in
let x0 = Map.set x0 0 3 in
x := Map.set !x 0 x0
let ghost proj_map_test1 (ghost x : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
=
x := Map.set !x 0 3
let ghost proj_map_test2 (ghost x : ref (map int bool)) : unit
ensures { !x[0] <> !x[1] }
=
x := Map.set !x 0 true
end
theory ModelMap
use map.Map
goal t1 : forall t:map int int, i : int.
get (set t 0 42) i = get t i
end
module OtherIndices
use map.Map
goal g : forall m: map real real. m 0.1 = 0.0 \/ m 0.2 = m 0.1
end
|
