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 \<open>Datatype_Records.mk_update_defs \<^type_name>\<open>AVLNode\<close>\<close>
(*[avl_verification::AVLTreeSet]
Source: 'src/main.rs', lines 18:0-18:17*)
datatype AVLTreeSet = mkAVLTreeSet (root: "AVLNode option")
local_setup \<open>Datatype_Records.mk_update_defs \<^type_name>\<open>AVLTreeSet\<close>\<close>
(*[avl_verification::{avl_verification::AVLTreeSet}::new]:
Source: 'src/main.rs', lines 23:4-23:24*)
definition aVLTreeSet_new :: "AVLTreeSet result" where
"aVLTreeSet_new = Ok (\<lparr> root = None \<rparr>)"
(*[avl_verification::cmp]:
Source: 'src/main.rs', lines 61:0-61:40*)
fun cmp :: "u32 \<Rightarrow> u32 \<Rightarrow> 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 \<Rightarrow> AVLNode option \<Rightarrow> (bool * AVLNode option) result" where
"aVLTreeSet_find_loop value1 current_tree =
(case current_tree of
None \<Rightarrow> Ok (False, None)
| Some current_node \<Rightarrow>
do {
o1 \<leftarrow> cmp (val current_node) value1;
(case o1 of
Ordering_Less \<Rightarrow>
do {
(b, current_tree1) \<leftarrow>
aVLTreeSet_find_loop value1 (right current_node);
Ok (b, Some
(current_node \<lparr> right := current_tree1 \<rparr>))
}
| Ordering_Equal \<Rightarrow> Ok (True, Some current_node)
| Ordering_Greater \<Rightarrow>
do {
(b, current_tree1) \<leftarrow>
aVLTreeSet_find_loop value1 (left current_node);
Ok (b, Some (current_node \<lparr> left := current_tree1 \<rparr>))
})
})" by auto
(*[avl_verification::{avl_verification::AVLTreeSet}::find]:
Source: 'src/main.rs', lines 27:4-27:46*)
fun aVLTreeSet_find
:: "AVLTreeSet \<Rightarrow> u32 \<Rightarrow> (bool * AVLTreeSet) result" where
"aVLTreeSet_find self value1 =
do {
(b, as) \<leftarrow> aVLTreeSet_find_loop value1 (root self);
Ok (b, (\<lparr> root = as \<rparr>))
}"
(*[avl_verification::{avl_verification::AVLTreeSet}::insert]: loop 0:
Source: 'src/main.rs', lines 40:4-58:5*)
function aVLTreeSet_insert_loop
:: "u32 \<Rightarrow> AVLNode option \<Rightarrow> (bool * AVLNode option) result" where
"aVLTreeSet_insert_loop value1 current_tree =
(case current_tree of
None \<Rightarrow>
let a = (\<lparr> val = value1, left = None, right = None \<rparr>) in
Ok (True, Some a)
| Some current_node \<Rightarrow>
do {
o1 \<leftarrow> cmp (val current_node) value1;
(case o1 of
Ordering_Less \<Rightarrow>
do {
(b, current_tree1) \<leftarrow>
aVLTreeSet_insert_loop value1 (right current_node);
Ok (b, Some
(current_node \<lparr> right := current_tree1 \<rparr>))
}
| Ordering_Equal \<Rightarrow> Ok (False, Some current_node)
| Ordering_Greater \<Rightarrow>
do {
(b, current_tree1) \<leftarrow>
aVLTreeSet_insert_loop value1 (left current_node);
Ok (b, Some (current_node \<lparr> left := current_tree1 \<rparr>))
})
})" by auto
(*[avl_verification::{avl_verification::AVLTreeSet}::insert]:
Source: 'src/main.rs', lines 40:4-40:48*)
fun aVLTreeSet_insert
:: "AVLTreeSet \<Rightarrow> u32 \<Rightarrow> (bool * AVLTreeSet) result" where
"aVLTreeSet_insert self value1 =
do {
(b, as) \<leftarrow> aVLTreeSet_insert_loop value1 (root self);
Ok (b, (\<lparr> root = as \<rparr>))
}"
end
|
