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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [avl_verification] *)
theory "Notraits" imports
"Aeneas.Primitives"
"HOL-Library.Datatype_Records"
begin
(*[avl_verification::Ordering]
Source: 'src/main.rs', lines 1:0-1:17*)
datatype Ordering = Ordering_Less | Ordering_Equal | Ordering_Greater
(*[avl_verification::AVLNode]
Source: 'src/main.rs', lines 10:0-10:14*)
datatype AVLNode = mkAVLNode
(val: "u32") (left: "AVLNode option") (right: "AVLNode option")
local_setup ‹Datatype_Records.mk_update_defs �‹AVLNode››
(*[avl_verification::AVLTreeSet]
Source: 'src/main.rs', lines 18:0-18:17*)
datatype AVLTreeSet = mkAVLTreeSet (root: "AVLNode option")
local_setup ‹Datatype_Records.mk_update_defs �‹AVLTreeSet››
(*[avl_verification::{avl_verification::AVLTreeSet}::new]:
Source: 'src/main.rs', lines 23:4-23:24*)
definition aVLTreeSet_new :: "AVLTreeSet result" where
"aVLTreeSet_new = Ok (⦇ root = None ⦈)"
(*[avl_verification::cmp]:
Source: 'src/main.rs', lines 61:0-61:40*)
fun cmp :: "u32 ⇒ u32 ⇒ Ordering result" where
"cmp a other =
(if u32_lt a other
then Ok Ordering_Less
else (if a = other then Ok Ordering_Equal else Ok Ordering_Greater))"
(*[avl_verification::{avl_verification::AVLTreeSet}::find]: loop 0:
Source: 'src/main.rs', lines 27:4-39:5*)
function aVLTreeSet_find_loop
:: "u32 ⇒ AVLNode option ⇒ (bool * AVLNode option) result" where
"aVLTreeSet_find_loop value1 current_tree =
(case current_tree of
None ⇒ Ok (False, None)
| Some current_node ⇒
do {
o1 ← cmp (val current_node) value1;
(case o1 of
Ordering_Less ⇒
do {
(b, current_tree1) ←
aVLTreeSet_find_loop value1 (right current_node);
Ok (b, Some
(current_node ⦇ right := current_tree1 ⦈))
}
| Ordering_Equal ⇒ Ok (True, Some current_node)
| Ordering_Greater ⇒
do {
(b, current_tree1) ←
aVLTreeSet_find_loop value1 (left current_node);
Ok (b, Some (current_node ⦇ left := current_tree1 ⦈))
})
})" by auto
(*[avl_verification::{avl_verification::AVLTreeSet}::find]:
Source: 'src/main.rs', lines 27:4-27:46*)
fun aVLTreeSet_find
:: "AVLTreeSet ⇒ u32 ⇒ (bool * AVLTreeSet) result" where
"aVLTreeSet_find self value1 =
do {
(b, as) ← aVLTreeSet_find_loop value1 (root self);
Ok (b, (⦇ root = as ⦈))
}"
(*[avl_verification::{avl_verification::AVLTreeSet}::insert]: loop 0:
Source: 'src/main.rs', lines 40:4-58:5*)
function aVLTreeSet_insert_loop
:: "u32 ⇒ AVLNode option ⇒ (bool * AVLNode option) result" where
"aVLTreeSet_insert_loop value1 current_tree =
(case current_tree of
None ⇒
let a = (⦇ val = value1, left = None, right = None ⦈) in
Ok (True, Some a)
| Some current_node ⇒
do {
o1 ← cmp (val current_node) value1;
(case o1 of
Ordering_Less ⇒
do {
(b, current_tree1) ←
aVLTreeSet_insert_loop value1 (right current_node);
Ok (b, Some
(current_node ⦇ right := current_tree1 ⦈))
}
| Ordering_Equal ⇒ Ok (False, Some current_node)
| Ordering_Greater ⇒
do {
(b, current_tree1) ←
aVLTreeSet_insert_loop value1 (left current_node);
Ok (b, Some (current_node ⦇ left := current_tree1 ⦈))
})
})" by auto
(*[avl_verification::{avl_verification::AVLTreeSet}::insert]:
Source: 'src/main.rs', lines 40:4-40:48*)
fun aVLTreeSet_insert
:: "AVLTreeSet ⇒ u32 ⇒ (bool * AVLTreeSet) result" where
"aVLTreeSet_insert self value1 =
do {
(b, as) ← aVLTreeSet_insert_loop value1 (root self);
Ok (b, (⦇ root = as ⦈))
}"
end
|
