| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1260 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (820 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (170 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (192 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
Global Index
A
add_another [lemma, in Verif_triang]add_list_sublist_bounds [lemma, in Verif_triang]
add_list_nonneg [lemma, in Verif_triang]
add_list_app [lemma, in Verif_triang]
add_list_decreasing_eq [lemma, in Verif_triang]
add_list_decreasing_eq_alt [lemma, in Verif_triang]
add_list [definition, in Verif_triang]
al:103 [binder, in Verif_hash]
al:108 [binder, in Verif_hash]
al:11 [binder, in Hashfun]
al:126 [binder, in Verif_hash]
al:130 [binder, in Verif_hash]
al:131 [binder, in Verif_hash]
al:139 [binder, in Verif_hash]
al:144 [binder, in Verif_hash]
al:178 [binder, in Verif_hash]
al:19 [binder, in Hashfun]
al:64 [binder, in Verif_hash]
al:65 [binder, in Verif_hash]
al:7 [binder, in Hashfun]
al:87 [binder, in Verif_triang]
append_spec [definition, in Verif_append1]
a:1 [binder, in Verif_triang]
a:1 [binder, in Verif_sumarray]
A:123 [binder, in Verif_hash]
a:21 [binder, in Verif_append1]
a:24 [binder, in Verif_append1]
a:25 [binder, in Verif_append2]
a:25 [binder, in Hashfun]
a:28 [binder, in Verif_append1]
a:3 [binder, in Verif_triang]
a:3 [binder, in Verif_sumarray]
a:38 [binder, in Verif_reverse]
A:42 [binder, in Verif_append2]
a:44 [binder, in Verif_reverse]
a:45 [binder, in Verif_append2]
A:47 [binder, in Verif_append2]
A:68 [binder, in Verif_hash]
a:8 [binder, in Verif_sumarray]
a:80 [binder, in Verif_append2]
a:86 [binder, in Verif_append1]
a:89 [binder, in Verif_append1]
a:96 [binder, in Verif_append1]
B
Bib [library]bl:122 [binder, in Verif_hash]
bl:75 [binder, in Verif_hash]
bl:88 [binder, in Verif_triang]
body_incr [lemma, in Verif_hash]
body_incr_field_address_lemma [lemma, in Verif_hash]
body_incr_list [lemma, in Verif_hash]
body_get [lemma, in Verif_hash]
body_new_table [lemma, in Verif_hash]
body_new_table_helper [lemma, in Verif_hash]
body_new_cell [lemma, in Verif_hash]
body_copy_string [lemma, in Verif_hash]
body_hash [lemma, in Verif_hash]
body_main [lemma, in VSU_main2]
body_append_alter2 [lemma, in Verif_append2]
body_exit [axiom, in VSU_stdlib]
body_free [axiom, in VSU_stdlib]
body_malloc [axiom, in VSU_stdlib]
body_exit [lemma, in VSU_stdlib2]
body_free [lemma, in VSU_stdlib2]
body_malloc [lemma, in VSU_stdlib2]
body_surely_malloc [lemma, in VSU_stack]
body_newstack [lemma, in VSU_stack]
body_push [lemma, in VSU_stack]
body_pop [lemma, in VSU_stack]
body_main [lemma, in Verif_triang]
body_pop_and_add [lemma, in Verif_triang]
body_pop_and_add [lemma, in Verif_triang]
body_push_increasing [lemma, in Verif_triang]
body_append_alter1 [lemma, in Verif_append1]
body_append [lemma, in Verif_append1]
body_main [lemma, in Verif_sumarray]
body_sumarray [lemma, in Verif_sumarray]
body_reverse_step [lemma, in Verif_reverse]
body_reverse [lemma, in Verif_reverse]
body_triang [lemma, in VSU_triang]
body_pop_and_add [lemma, in VSU_triang]
body_push_increasing [lemma, in VSU_triang]
body_main [lemma, in VSU_main]
body_strcmp [lemma, in Verif_strlib]
body_example_call_strcpy [lemma, in Verif_strlib]
body_strcpy [lemma, in Verif_strlib]
body_strlen [lemma, in Verif_strlib]
body_newstack [lemma, in Verif_stack]
body_push [lemma, in Verif_stack]
body_pop [lemma, in Verif_stack]
b0:142 [binder, in Verif_hash]
b:148 [binder, in Verif_hash]
b:150 [binder, in Verif_hash]
b:2 [binder, in Verif_triang]
b:2 [binder, in Verif_sumarray]
b:25 [binder, in Verif_append1]
b:29 [binder, in Verif_append1]
b:33 [binder, in Verif_append2]
b:38 [binder, in Verif_append2]
b:39 [binder, in Verif_reverse]
b:4 [binder, in Verif_triang]
b:45 [binder, in Verif_reverse]
b:54 [binder, in Verif_append1]
b:59 [binder, in Verif_append1]
B:69 [binder, in Verif_hash]
b:90 [binder, in Verif_append1]
C
cancel_example [lemma, in Verif_strlib]CompSpecs [instance, in Verif_hash]
Compspecs [instance, in VSU_main2]
CompSpecs [instance, in VSU_stdlib]
CompSpecs [instance, in VSU_stdlib2]
CompSpecs [instance, in VSU_stack]
CompSpecs [instance, in Verif_triang]
CompSpecs [instance, in Verif_append1]
CompSpecs [instance, in Verif_sumarray]
CompSpecs [instance, in Verif_reverse]
CompSpecs [instance, in VSU_triang]
Compspecs [instance, in VSU_main]
CompSpecs [instance, in VSU_main]
CompSpecs [instance, in Verif_strlib]
CompSpecs [instance, in Verif_stack]
contents:10 [binder, in Verif_sumarray]
contents:11 [binder, in Verif_strlib]
contents:113 [binder, in Verif_hash]
contents:118 [binder, in Verif_hash]
contents:15 [binder, in Verif_append2]
contents:15 [binder, in Verif_append1]
contents:15 [binder, in Hashfun]
contents:17 [binder, in Hashfun]
contents:30 [binder, in Verif_hash]
contents:32 [binder, in Verif_hash]
contents:46 [binder, in Verif_append1]
contents:48 [binder, in Verif_append1]
contents:5 [binder, in Verif_sumarray]
contents:54 [binder, in Verif_append2]
contents:57 [binder, in Verif_append2]
contents:6 [binder, in Verif_strlib]
contents:73 [binder, in Verif_hash]
contents:76 [binder, in Verif_hash]
contents:78 [binder, in Verif_hash]
contents:79 [binder, in Verif_append1]
contents:85 [binder, in Verif_append1]
contents:95 [binder, in Verif_hash]
contents:99 [binder, in Verif_hash]
copy_string_spec [definition, in Verif_hash]
coreVSU [definition, in VSU_main2]
coreVSU [definition, in VSU_main]
COUNT_TABLE.gso [axiom, in Hashfun]
COUNT_TABLE.gss [axiom, in Hashfun]
COUNT_TABLE.gempty [axiom, in Hashfun]
COUNT_TABLE.incr [axiom, in Hashfun]
COUNT_TABLE.get [axiom, in Hashfun]
COUNT_TABLE.empty [axiom, in Hashfun]
COUNT_TABLE.key [axiom, in Hashfun]
COUNT_TABLE.table [axiom, in Hashfun]
COUNT_TABLE [module, in Hashfun]
count:133 [binder, in Verif_hash]
count:138 [binder, in Verif_hash]
count:155 [binder, in Verif_hash]
count:161 [binder, in Verif_hash]
count:34 [binder, in Verif_hash]
count:39 [binder, in Verif_hash]
count:43 [binder, in Verif_hash]
count:48 [binder, in Verif_hash]
count:61 [binder, in Verif_hash]
count:85 [binder, in Verif_hash]
count:90 [binder, in Verif_hash]
cs:12 [binder, in VSU_stdlib]
cs:26 [binder, in Spec_stdlib]
cs:31 [binder, in Spec_stdlib]
cs:36 [binder, in Spec_stdlib]
cs:42 [binder, in Spec_stdlib]
cs:48 [binder, in Spec_stdlib]
cs:5 [binder, in VSU_stdlib]
cs:55 [binder, in Spec_stdlib]
cs:58 [binder, in Spec_stdlib]
cs:8 [binder, in VSU_stdlib]
cts:146 [binder, in Verif_hash]
cts:147 [binder, in Verif_hash]
cts:180 [binder, in Verif_hash]
cts:181 [binder, in Verif_hash]
cts:22 [binder, in Hashfun]
cts:24 [binder, in Hashfun]
cts:58 [binder, in Hashfun]
cts:62 [binder, in Hashfun]
c:30 [binder, in Verif_append1]
C:70 [binder, in Verif_hash]
D
data_at_thashtable_tarray [lemma, in Verif_hash]data_at_isptr_example2 [lemma, in Verif_reverse]
data_at_isptr_example1 [lemma, in Verif_reverse]
data_at_Vundef_example [lemma, in Verif_strlib]
data_at_Vundef_example [lemma, in Verif_strlib]
decreasing_Z1 [definition, in Verif_triang]
decreasing_Z1_aux [definition, in Verif_triang]
decreasing_Z [definition, in Verif_triang]
decreasing_nat [definition, in Verif_triang]
demonstrate_cstring2 [lemma, in Verif_strlib]
demonstrate_cstring1 [lemma, in Verif_strlib]
dest:10 [binder, in Verif_hash]
dest:14 [binder, in Verif_hash]
dest:23 [binder, in Verif_strlib]
dest:29 [binder, in Verif_strlib]
dest:51 [binder, in Verif_strlib]
dest:55 [binder, in Verif_strlib]
Digression [module, in VSU_stdlib2]
Digression.N [definition, in VSU_stdlib2]
Digression.N_eq [definition, in VSU_stdlib2]
Digression.N' [definition, in VSU_stdlib2]
Digression.N'' [definition, in VSU_stdlib2]
dl:157 [binder, in Verif_hash]
dl:163 [binder, in Verif_hash]
d:124 [binder, in Verif_hash]
E
empty_table [definition, in Hashfun]emp_lbseg [lemma, in Verif_append2]
emp_wlseg [lemma, in Verif_append2]
emp_wand_emp_left [lemma, in Verif_append2]
emp_wand_emp_right [lemma, in Verif_append2]
EqDec_string [instance, in Hashfun]
Espec:10 [binder, in VSU_stdlib]
Espec:4 [binder, in VSU_stdlib]
Espec:50 [binder, in Verif_reverse]
Espec:7 [binder, in VSU_stdlib]
example_field_at_data_at''' [lemma, in Verif_hash]
example_field_at_data_at'' [lemma, in Verif_hash]
example_field_at_data_at' [lemma, in Verif_hash]
example_field_at_data_at [lemma, in Verif_hash]
example_split_struct [lemma, in Verif_hash]
example_call_strcpy_spec [definition, in Verif_strlib]
exit_spec [definition, in Spec_stdlib]
F
four_contents [definition, in Verif_sumarray]freelistrep [definition, in VSU_stdlib2]
freelistrep_valid_pointer [lemma, in VSU_stdlib2]
freelistrep_local_prop [lemma, in VSU_stdlib2]
frees:22 [binder, in VSU_stdlib2]
free_spec_sub [lemma, in Spec_stdlib]
free_spec [definition, in Spec_stdlib]
free_spec_sz [definition, in Spec_stdlib]
free_spec_example [definition, in Verif_stack]
FunTable [module, in Hashfun]
FunTable.empty [definition, in Hashfun]
FunTable.gempty [lemma, in Hashfun]
FunTable.get [definition, in Hashfun]
FunTable.gso [lemma, in Hashfun]
FunTable.gss [lemma, in Hashfun]
FunTable.incr [definition, in Hashfun]
FunTable.key [definition, in Hashfun]
FunTable.table [definition, in Hashfun]
f:127 [binder, in Verif_hash]
f:16 [binder, in Verif_sumarray]
f:71 [binder, in Verif_hash]
G
get_spec [definition, in Verif_hash]Gprog [definition, in Verif_hash]
Gprog [definition, in Verif_triang]
Gprog [definition, in Verif_append1]
Gprog [definition, in Verif_sumarray]
Gprog [definition, in Verif_reverse]
Gprog [definition, in Verif_strlib]
Gprog [definition, in Verif_stack]
gv:1 [binder, in VSU_main2]
gv:1 [binder, in VSU_main]
gv:106 [binder, in Verif_hash]
gv:11 [binder, in Spec_stack]
gv:11 [binder, in Verif_stack]
gv:111 [binder, in Verif_hash]
gv:116 [binder, in Verif_hash]
gv:12 [binder, in Verif_sumarray]
gv:12 [binder, in Spec_stack]
gv:121 [binder, in Verif_hash]
gv:13 [binder, in VSU_stdlib]
gv:13 [binder, in Verif_sumarray]
gv:14 [binder, in Spec_stdlib]
gv:16 [binder, in Spec_stdlib]
gv:17 [binder, in Spec_stack]
gv:19 [binder, in VSU_stdlib2]
gv:19 [binder, in VSU_stack]
gv:2 [binder, in VSU_main2]
gv:2 [binder, in VSU_stdlib]
gv:2 [binder, in Spec_triang]
gv:2 [binder, in VSU_main]
gv:2 [binder, in Verif_stack]
gv:20 [binder, in Spec_stdlib]
gv:21 [binder, in VSU_stack]
gv:21 [binder, in Spec_stack]
gv:23 [binder, in Spec_stdlib]
gv:23 [binder, in VSU_stdlib2]
gv:24 [binder, in Verif_hash]
gv:25 [binder, in Spec_stack]
gv:27 [binder, in Verif_hash]
gv:28 [binder, in Verif_stack]
gv:29 [binder, in Spec_stack]
gv:29 [binder, in Verif_stack]
gv:3 [binder, in Spec_triang]
gv:34 [binder, in Verif_stack]
gv:38 [binder, in Verif_stack]
gv:4 [binder, in Verif_stack]
gv:42 [binder, in Verif_stack]
gv:44 [binder, in Spec_stdlib]
gv:45 [binder, in Spec_stdlib]
gv:46 [binder, in Verif_stack]
gv:51 [binder, in Spec_stdlib]
gv:53 [binder, in Spec_stdlib]
gv:54 [binder, in Verif_triang]
gv:55 [binder, in Verif_triang]
gv:60 [binder, in Verif_triang]
gv:64 [binder, in Verif_triang]
gv:68 [binder, in Verif_triang]
gv:72 [binder, in Verif_triang]
gv:74 [binder, in Verif_strlib]
gv:75 [binder, in Verif_triang]
gv:75 [binder, in Verif_strlib]
gv:78 [binder, in Verif_triang]
gv:8 [binder, in Verif_stack]
gv:80 [binder, in Verif_hash]
gv:81 [binder, in Verif_hash]
gv:81 [binder, in Verif_triang]
gv:84 [binder, in Verif_triang]
gv:85 [binder, in Verif_triang]
gv:86 [binder, in Verif_triang]
gv:87 [binder, in Verif_hash]
gv:92 [binder, in Verif_hash]
gx:14 [binder, in VSU_stdlib]
H
hashfun [definition, in Hashfun]Hashfun [library]
hashfun_snoc [lemma, in Hashfun]
hashfun_aux_snoc [lemma, in Hashfun]
hashfun_inrange [lemma, in Hashfun]
hashfun_aux [definition, in Hashfun]
hashtable_rep_valid_pointer [lemma, in Verif_hash]
hashtable_rep_local_facts [lemma, in Verif_hash]
hashtable_rep [definition, in Verif_hash]
hashtable_get_unfold [lemma, in Hashfun]
hashtable_incr [definition, in Hashfun]
hashtable_get [definition, in Hashfun]
hashtable_contents [definition, in Hashfun]
hash_spec [definition, in Verif_hash]
Hello [definition, in Verif_strlib]
Hello' [definition, in Verif_strlib]
hi:91 [binder, in Verif_triang]
HRE:57 [binder, in Verif_reverse]
hs:51 [binder, in Verif_append1]
H0:13 [binder, in Verif_strlib]
H0:8 [binder, in Verif_strlib]
H1:14 [binder, in Verif_strlib]
H1:9 [binder, in Verif_strlib]
h:1 [binder, in Hashfun]
H:12 [binder, in Verif_strlib]
h:177 [binder, in Verif_hash]
h:18 [binder, in Verif_reverse]
h:18 [binder, in Hashfun]
h:27 [binder, in Hashfun]
h:50 [binder, in Verif_append1]
h:53 [binder, in Verif_reverse]
H:58 [binder, in Verif_reverse]
h:6 [binder, in Verif_reverse]
H:7 [binder, in Verif_strlib]
h:9 [binder, in Verif_reverse]
I
il:11 [binder, in VSU_stack]il:12 [binder, in Verif_stack]
il:14 [binder, in VSU_stack]
il:16 [binder, in VSU_stack]
il:16 [binder, in Spec_stack]
il:17 [binder, in Verif_stack]
il:19 [binder, in Verif_stack]
il:2 [binder, in VSU_stack]
il:20 [binder, in Spec_stack]
il:21 [binder, in Verif_stack]
il:24 [binder, in Spec_stack]
il:24 [binder, in Verif_stack]
il:26 [binder, in Verif_stack]
il:28 [binder, in Spec_stack]
il:3 [binder, in Spec_stack]
il:33 [binder, in Verif_stack]
il:37 [binder, in Verif_stack]
il:38 [binder, in Verif_triang]
il:41 [binder, in Verif_stack]
il:43 [binder, in Verif_triang]
il:45 [binder, in Verif_triang]
il:45 [binder, in Verif_stack]
il:47 [binder, in Verif_triang]
il:50 [binder, in Verif_triang]
il:52 [binder, in Verif_triang]
il:59 [binder, in Verif_triang]
il:6 [binder, in Spec_stack]
il:63 [binder, in Verif_triang]
il:67 [binder, in Verif_triang]
il:7 [binder, in VSU_stack]
il:71 [binder, in Verif_triang]
il:80 [binder, in Verif_triang]
il:83 [binder, in Verif_triang]
il:89 [binder, in Verif_triang]
il:9 [binder, in VSU_stack]
il:93 [binder, in Verif_triang]
il:94 [binder, in Verif_triang]
implies_and_adjoint [lemma, in Verif_append2]
incr_spec [definition, in Verif_hash]
incr_list_spec [definition, in Verif_hash]
initialize [lemma, in VSU_stdlib]
initialize [lemma, in VSU_stdlib2]
IntHashTable [module, in Hashfun]
IntHashTable.empty [definition, in Hashfun]
IntHashTable.empty_invariant [lemma, in Hashfun]
IntHashTable.gempty [lemma, in Hashfun]
IntHashTable.get [definition, in Hashfun]
IntHashTable.gso [lemma, in Hashfun]
IntHashTable.gss [lemma, in Hashfun]
IntHashTable.hashtable_invariant [definition, in Hashfun]
IntHashTable.incr [definition, in Hashfun]
IntHashTable.incr_invariant [lemma, in Hashfun]
IntHashTable.key [definition, in Hashfun]
IntHashTable.table [definition, in Hashfun]
Int_repr_eq_mod [lemma, in Hashfun]
iter_sepcon_split3 [lemma, in Verif_hash]
iter_sepcon_listrep_local_facts [lemma, in Verif_hash]
i:10 [binder, in Verif_strlib]
i:125 [binder, in Verif_hash]
i:14 [binder, in Verif_sumarray]
i:15 [binder, in Verif_sumarray]
i:15 [binder, in Spec_stack]
i:18 [binder, in Verif_sumarray]
i:19 [binder, in Spec_stack]
i:20 [binder, in VSU_stdlib2]
i:23 [binder, in Spec_stack]
i:24 [binder, in Spec_stdlib]
i:25 [binder, in Spec_stdlib]
i:27 [binder, in Spec_stack]
i:29 [binder, in Hashfun]
i:31 [binder, in Hashfun]
i:32 [binder, in Verif_stack]
i:34 [binder, in Verif_triang]
i:36 [binder, in Verif_stack]
i:40 [binder, in Verif_stack]
i:44 [binder, in Verif_stack]
i:45 [binder, in Verif_strlib]
i:46 [binder, in Verif_strlib]
i:47 [binder, in Verif_strlib]
i:5 [binder, in Verif_strlib]
i:58 [binder, in Verif_triang]
i:58 [binder, in Verif_strlib]
i:59 [binder, in Verif_strlib]
i:59 [binder, in Hashfun]
i:62 [binder, in Verif_triang]
i:63 [binder, in Verif_strlib]
i:66 [binder, in Verif_triang]
i:68 [binder, in Verif_strlib]
i:70 [binder, in Verif_triang]
i:72 [binder, in Verif_strlib]
i:73 [binder, in Verif_strlib]
i:9 [binder, in Verif_hash]
i:95 [binder, in Verif_triang]
i:96 [binder, in Verif_triang]
i:97 [binder, in Verif_triang]
J
j:42 [binder, in Hashfun]j:55 [binder, in Hashfun]
j:69 [binder, in Verif_strlib]
j:70 [binder, in Hashfun]
K
key:132 [binder, in Verif_hash]key:137 [binder, in Verif_hash]
key:154 [binder, in Verif_hash]
key:160 [binder, in Verif_hash]
key:33 [binder, in Verif_hash]
key:38 [binder, in Verif_hash]
key:42 [binder, in Verif_hash]
key:46 [binder, in Verif_hash]
key:60 [binder, in Verif_hash]
key:84 [binder, in Verif_hash]
key:89 [binder, in Verif_hash]
kp:136 [binder, in Verif_hash]
kp:153 [binder, in Verif_hash]
kp:159 [binder, in Verif_hash]
kp:37 [binder, in Verif_hash]
kp:47 [binder, in Verif_hash]
k':51 [binder, in Hashfun]
k:37 [binder, in Hashfun]
k:39 [binder, in Hashfun]
k:43 [binder, in Hashfun]
k:46 [binder, in Hashfun]
k:47 [binder, in Hashfun]
k:49 [binder, in Hashfun]
k:52 [binder, in Hashfun]
k:53 [binder, in Hashfun]
k:56 [binder, in Hashfun]
k:61 [binder, in Hashfun]
k:63 [binder, in Hashfun]
k:65 [binder, in Hashfun]
k:67 [binder, in Hashfun]
k:68 [binder, in Hashfun]
k:71 [binder, in Hashfun]
K:92 [binder, in Verif_triang]
L
lbseg [definition, in Verif_append2]lbseg_lbseg [lemma, in Verif_append2]
listboxrep [definition, in Verif_hash]
listboxrep [definition, in Verif_append2]
listboxrep_traverse32 [lemma, in Verif_hash]
listboxrep_traverse [lemma, in Verif_hash]
listbox_lbseg [lemma, in Verif_append2]
listcell_fold [lemma, in Verif_hash]
listrep [definition, in Verif_hash]
listrep [definition, in VSU_stack]
listrep [definition, in Verif_triang]
listrep [definition, in Verif_append1]
listrep [definition, in Verif_reverse]
listrep [definition, in Verif_stack]
listrep_traverse_finish [lemma, in Verif_hash]
listrep_traverse_step_example [lemma, in Verif_hash]
listrep_traverse_step [lemma, in Verif_hash]
listrep_traverse_start [lemma, in Verif_hash]
listrep_fold [lemma, in Verif_hash]
listrep_valid_pointer [lemma, in Verif_hash]
listrep_local_prop [lemma, in Verif_hash]
listrep_valid_pointer [lemma, in VSU_stack]
listrep_local_prop [lemma, in VSU_stack]
listrep_valid_pointer [lemma, in Verif_triang]
listrep_local_prop [lemma, in Verif_triang]
listrep_nonnull [lemma, in Verif_append1]
listrep_null [lemma, in Verif_append1]
listrep_valid_pointer [lemma, in Verif_append1]
listrep_local_facts [lemma, in Verif_append1]
listrep_len_ge2_address_different [lemma, in Verif_reverse]
listrep_len_ge2_fact [lemma, in Verif_reverse]
listrep_valid_pointer [lemma, in Verif_reverse]
listrep_valid_pointer_example [lemma, in Verif_reverse]
listrep_local_facts [lemma, in Verif_reverse]
listrep_facts_example [lemma, in Verif_reverse]
listrep_facts_example [lemma, in Verif_reverse]
listrep_valid_pointer [lemma, in Verif_stack]
listrep_local_prop [lemma, in Verif_stack]
listrep2lseg [lemma, in Verif_append1]
list_cell_valid_pointer [definition, in Verif_hash]
list_cell_local_facts [definition, in Verif_hash]
list_cell [definition, in Verif_hash]
list_incr [definition, in Hashfun]
list_get [definition, in Hashfun]
loopy_lseg_no_connection [lemma, in Verif_append1]
loopy_lseg_not_bad [lemma, in Verif_append1]
lo:28 [binder, in Hashfun]
lo:90 [binder, in Verif_triang]
lseg [definition, in Verif_append1]
lseg_lseg_inv [lemma, in Verif_append1]
lseg_listrep_equiv [lemma, in Verif_append1]
lseg_list [lemma, in Verif_append1]
lseg_lseg [lemma, in Verif_append1]
lseg_maybe_loop [lemma, in Verif_append1]
lseg2listrep [lemma, in Verif_append1]
lseg2wlseg [lemma, in Verif_append2]
l:41 [binder, in Verif_reverse]
l:49 [binder, in Verif_reverse]
M
M [definition, in VSU_main2]M [axiom, in VSU_stdlib]
M [definition, in VSU_stdlib2]
M [definition, in VSU_main]
MainComp [definition, in VSU_main2]
MainComp [definition, in VSU_main]
Main_Gprog [definition, in VSU_main2]
Main_imports [definition, in VSU_main2]
main_spec [definition, in VSU_main2]
main_spec [definition, in Verif_triang]
main_spec [definition, in Verif_sumarray]
Main_Gprog [definition, in VSU_main]
Main_imports [definition, in VSU_main]
main_spec [definition, in VSU_main]
make_mem_mgr [axiom, in VSU_stdlib]
MallocFreeAPD [record, in Spec_stdlib]
MallocFreeASI [definition, in Spec_stdlib]
MallocFreeASI [section, in Spec_stdlib]
MallocFreeASI.M [variable, in Spec_stdlib]
MallocFreeVSU [definition, in VSU_stdlib]
MallocFreeVSU [definition, in VSU_stdlib2]
malloc_spec_sub [lemma, in Spec_stdlib]
malloc_spec [definition, in Spec_stdlib]
malloc_token_local_facts [lemma, in Spec_stdlib]
malloc_token_valid_pointer [lemma, in Spec_stdlib]
malloc_token [definition, in Spec_stdlib]
malloc_spec_sz [definition, in Spec_stdlib]
malloc_token_sz_local_facts [projection, in Spec_stdlib]
malloc_token_sz_valid_pointer [projection, in Spec_stdlib]
malloc_token_sz [projection, in Spec_stdlib]
malloc_token_sz_local_facts [lemma, in VSU_stdlib2]
malloc_token_sz_valid_pointer [lemma, in VSU_stdlib2]
malloc_token_sz [definition, in VSU_stdlib2]
malloc_spec_example [definition, in Verif_stack]
mem_mgr [projection, in Spec_stdlib]
mem_mgr [definition, in VSU_stdlib2]
MFGprog [definition, in VSU_stdlib]
MFGprog [definition, in VSU_stdlib2]
MFVprog [definition, in VSU_stdlib]
MFVprog [definition, in VSU_stdlib2]
MF_E [definition, in VSU_stdlib]
MF_globals [definition, in VSU_stdlib]
MF_internal_specs [definition, in VSU_stdlib]
MF_imported_specs [definition, in VSU_stdlib]
MF_ASI [definition, in VSU_stdlib]
MF_Externs [definition, in VSU_stdlib2]
MF_globals [definition, in VSU_stdlib2]
MF_internal_specs [definition, in VSU_stdlib2]
MF_imported_specs [definition, in VSU_stdlib2]
MF_ASI [definition, in VSU_stdlib2]
modus_ponens_wand_from_adjoint [lemma, in Verif_append2]
M:27 [binder, in Spec_stdlib]
M:32 [binder, in Spec_stdlib]
M:37 [binder, in Spec_stdlib]
M:41 [binder, in Spec_stdlib]
M:47 [binder, in Spec_stdlib]
M:54 [binder, in Spec_stdlib]
M:57 [binder, in Spec_stdlib]
N
N [definition, in VSU_stdlib2]N [definition, in Hashfun]
nat_sub_add_yuck [lemma, in Verif_triang]
newstack_spec [definition, in Verif_triang]
newstack_spec [definition, in Spec_stack]
newstack_spec [definition, in Verif_stack]
new_cell_spec [definition, in Verif_hash]
new_table_spec [definition, in Verif_hash]
next:35 [binder, in Verif_hash]
next:40 [binder, in Verif_hash]
next:44 [binder, in Verif_hash]
next:86 [binder, in Verif_hash]
next:91 [binder, in Verif_hash]
nt_lseg_list [lemma, in Verif_append1]
nt_lseg_nt_lseg [lemma, in Verif_append1]
nt_lseg [definition, in Verif_append1]
N_eq [definition, in VSU_stdlib2]
N_eq [lemma, in Hashfun]
n:1 [binder, in VSU_stdlib2]
n:11 [binder, in Verif_hash]
n:11 [binder, in VSU_stdlib2]
n:11 [binder, in Verif_triang]
n:128 [binder, in Verif_hash]
n:13 [binder, in Spec_stdlib]
n:14 [binder, in Verif_triang]
n:15 [binder, in Verif_hash]
n:15 [binder, in Spec_stdlib]
n:15 [binder, in Verif_triang]
n:16 [binder, in VSU_stdlib]
n:17 [binder, in Verif_triang]
n:18 [binder, in Spec_stdlib]
n:18 [binder, in Verif_triang]
n:20 [binder, in Verif_triang]
n:21 [binder, in Spec_stdlib]
n:21 [binder, in Verif_triang]
n:22 [binder, in Verif_triang]
n:24 [binder, in Verif_strlib]
n:30 [binder, in Verif_strlib]
n:35 [binder, in Verif_triang]
n:36 [binder, in Verif_triang]
n:37 [binder, in Verif_triang]
n:48 [binder, in Verif_strlib]
n:49 [binder, in Verif_strlib]
n:5 [binder, in Verif_triang]
n:52 [binder, in Verif_strlib]
n:56 [binder, in Verif_strlib]
n:6 [binder, in VSU_stdlib2]
n:60 [binder, in Verif_strlib]
n:64 [binder, in Verif_strlib]
n:74 [binder, in Verif_triang]
n:77 [binder, in Verif_triang]
n:8 [binder, in VSU_stdlib2]
n:8 [binder, in Verif_triang]
P
placeholder_spec [definition, in VSU_stdlib]pop_and_add_spec [definition, in Verif_triang]
pop_spec [definition, in Verif_triang]
pop_spec [definition, in Spec_stack]
pop_and_add_spec [definition, in VSU_triang]
pop_spec [definition, in Verif_stack]
Postscript [library]
Preface [library]
prog_correct [lemma, in Verif_sumarray]
push_increasing_spec [definition, in Verif_triang]
push_spec [definition, in Verif_triang]
push_spec [definition, in Spec_stack]
push_increasing_spec [definition, in VSU_triang]
push_spec [definition, in Verif_stack]
p':134 [binder, in Verif_hash]
p':49 [binder, in Verif_hash]
p':62 [binder, in Verif_hash]
P':9 [binder, in Verif_append2]
p0:143 [binder, in Verif_hash]
P:1 [binder, in Verif_append2]
p:10 [binder, in Spec_stdlib]
p:10 [binder, in VSU_stack]
p:10 [binder, in Verif_stack]
p:11 [binder, in Verif_reverse]
p:112 [binder, in Verif_hash]
p:117 [binder, in Verif_hash]
P:12 [binder, in Verif_append2]
p:12 [binder, in VSU_stdlib2]
p:12 [binder, in VSU_stack]
p:129 [binder, in Verif_hash]
p:13 [binder, in Verif_reverse]
p:13 [binder, in Spec_stack]
p:13 [binder, in Verif_stack]
p:135 [binder, in Verif_hash]
p:14 [binder, in Spec_stack]
p:141 [binder, in Verif_hash]
p:145 [binder, in Verif_hash]
p:149 [binder, in Verif_hash]
p:15 [binder, in VSU_stdlib2]
p:15 [binder, in VSU_stack]
p:15 [binder, in Verif_reverse]
p:151 [binder, in Verif_hash]
p:152 [binder, in Verif_hash]
p:158 [binder, in Verif_hash]
p:164 [binder, in Verif_hash]
p:168 [binder, in Verif_hash]
p:17 [binder, in Spec_stdlib]
p:17 [binder, in VSU_stack]
p:17 [binder, in Verif_reverse]
p:170 [binder, in Verif_hash]
p:172 [binder, in Verif_hash]
p:174 [binder, in Verif_hash]
p:18 [binder, in VSU_stdlib2]
p:18 [binder, in Spec_stack]
p:18 [binder, in Verif_stack]
p:19 [binder, in Spec_stdlib]
p:2 [binder, in VSU_stdlib2]
p:2 [binder, in Verif_append1]
p:2 [binder, in Verif_reverse]
p:20 [binder, in Verif_reverse]
p:20 [binder, in Verif_stack]
p:21 [binder, in VSU_stdlib2]
p:22 [binder, in Spec_stdlib]
p:22 [binder, in VSU_stack]
p:22 [binder, in Verif_reverse]
p:22 [binder, in Spec_stack]
p:22 [binder, in Verif_stack]
p:24 [binder, in Verif_reverse]
p:25 [binder, in Verif_stack]
p:26 [binder, in Verif_reverse]
p:26 [binder, in Spec_stack]
p:27 [binder, in Verif_stack]
p:28 [binder, in Verif_hash]
p:28 [binder, in Verif_reverse]
p:3 [binder, in VSU_stack]
p:30 [binder, in Verif_stack]
p:31 [binder, in Verif_stack]
P:33 [binder, in Verif_triang]
p:35 [binder, in Spec_stdlib]
p:35 [binder, in Verif_stack]
p:36 [binder, in Verif_hash]
p:39 [binder, in Verif_triang]
p:39 [binder, in Verif_stack]
P:4 [binder, in Verif_append2]
p:4 [binder, in Spec_stack]
p:40 [binder, in Spec_stdlib]
p:41 [binder, in Verif_hash]
P:43 [binder, in Verif_append2]
p:43 [binder, in Verif_append1]
p:43 [binder, in Verif_stack]
p:44 [binder, in Verif_triang]
p:45 [binder, in Verif_hash]
p:45 [binder, in Verif_append1]
p:46 [binder, in Spec_stdlib]
p:46 [binder, in Verif_triang]
P:48 [binder, in Verif_append2]
p:48 [binder, in Verif_triang]
p:5 [binder, in Verif_stack]
p:50 [binder, in Verif_hash]
p:50 [binder, in Spec_stdlib]
p:51 [binder, in Verif_triang]
p:52 [binder, in Spec_stdlib]
p:53 [binder, in Verif_triang]
p:56 [binder, in Verif_triang]
p:57 [binder, in Verif_hash]
p:57 [binder, in Verif_triang]
p:59 [binder, in Verif_hash]
P:6 [binder, in Verif_append2]
p:6 [binder, in Spec_stdlib]
p:61 [binder, in Verif_triang]
p:62 [binder, in Verif_strlib]
p:63 [binder, in Verif_hash]
p:65 [binder, in Verif_triang]
p:66 [binder, in Verif_strlib]
p:67 [binder, in Verif_hash]
p:69 [binder, in Verif_triang]
p:7 [binder, in VSU_stdlib2]
p:7 [binder, in Spec_stack]
p:7 [binder, in Verif_stack]
p:70 [binder, in Verif_strlib]
p:74 [binder, in Verif_hash]
p:77 [binder, in Verif_hash]
p:79 [binder, in Verif_hash]
P:8 [binder, in Verif_append2]
p:8 [binder, in VSU_stack]
p:8 [binder, in Verif_reverse]
p:82 [binder, in Verif_hash]
p:9 [binder, in VSU_stdlib2]
p:93 [binder, in Verif_hash]
p:94 [binder, in Verif_hash]
p:98 [binder, in Verif_hash]
Q
Q':11 [binder, in Verif_append2]Q:10 [binder, in Verif_append2]
Q:13 [binder, in Verif_append2]
q:13 [binder, in VSU_stack]
q:140 [binder, in Verif_hash]
Q:2 [binder, in Verif_append2]
q:23 [binder, in Verif_stack]
q:29 [binder, in Verif_reverse]
Q:44 [binder, in Verif_append2]
Q:49 [binder, in Verif_append2]
q:49 [binder, in Verif_triang]
Q:5 [binder, in Verif_append2]
Q:7 [binder, in Verif_append2]
q:71 [binder, in Verif_strlib]
R
release_needed [definition, in Preface]ret:15 [binder, in VSU_stdlib]
reverse_spec [definition, in Verif_reverse]
rsh:22 [binder, in Verif_strlib]
rsh:28 [binder, in Verif_strlib]
r0:102 [binder, in Verif_hash]
r0:107 [binder, in Verif_hash]
R:14 [binder, in Verif_append2]
r:14 [binder, in Verif_append1]
r:156 [binder, in Verif_hash]
r:162 [binder, in Verif_hash]
R:3 [binder, in Verif_append2]
R:50 [binder, in Verif_append2]
r:54 [binder, in Verif_reverse]
r:66 [binder, in Verif_hash]
S
semax_func_cons_malloc_aux [lemma, in VSU_stdlib]sh1:33 [binder, in Verif_strlib]
sh1:39 [binder, in Verif_strlib]
sh2:34 [binder, in Verif_strlib]
sh2:40 [binder, in Verif_strlib]
sh:10 [binder, in VSU_stdlib2]
sh:13 [binder, in VSU_stdlib2]
sh:15 [binder, in Verif_strlib]
sh:16 [binder, in VSU_stdlib2]
sh:18 [binder, in Verif_strlib]
sh:28 [binder, in Spec_stdlib]
sh:33 [binder, in Spec_stdlib]
sh:38 [binder, in Spec_stdlib]
sh:4 [binder, in Spec_stdlib]
sh:4 [binder, in Verif_sumarray]
sh:61 [binder, in Verif_strlib]
sh:65 [binder, in Verif_strlib]
sh:67 [binder, in Verif_strlib]
sh:8 [binder, in Spec_stdlib]
sh:9 [binder, in Verif_sumarray]
sigma:1 [binder, in Verif_append1]
sigma:1 [binder, in Verif_reverse]
sigma:101 [binder, in Verif_hash]
sigma:105 [binder, in Verif_hash]
sigma:110 [binder, in Verif_hash]
sigma:115 [binder, in Verif_hash]
sigma:12 [binder, in Verif_reverse]
sigma:120 [binder, in Verif_hash]
sigma:14 [binder, in Verif_reverse]
sigma:16 [binder, in Verif_reverse]
sigma:21 [binder, in Verif_reverse]
sigma:21 [binder, in Hashfun]
sigma:23 [binder, in Verif_hash]
sigma:23 [binder, in Verif_reverse]
sigma:23 [binder, in Hashfun]
sigma:25 [binder, in Verif_reverse]
sigma:26 [binder, in Verif_hash]
sigma:26 [binder, in Hashfun]
sigma:27 [binder, in Verif_reverse]
sigma:30 [binder, in Hashfun]
sigma:42 [binder, in Verif_append1]
sigma:44 [binder, in Verif_append1]
sigma:51 [binder, in Verif_hash]
sigma:51 [binder, in Verif_reverse]
sigma:56 [binder, in Verif_hash]
sigma:58 [binder, in Verif_hash]
sigma:97 [binder, in Verif_hash]
singleton_wlseg [lemma, in Verif_append2]
singleton_nt_lseg' [lemma, in Verif_append1]
singleton_nt_lseg [lemma, in Verif_append1]
singleton_lseg [lemma, in Verif_append1]
size:11 [binder, in Verif_sumarray]
size:6 [binder, in Verif_sumarray]
Spec_stdlib [library]
Spec_stack [library]
Spec_triang [library]
src:12 [binder, in Verif_hash]
src:16 [binder, in Verif_hash]
src:25 [binder, in Verif_strlib]
src:31 [binder, in Verif_strlib]
STACK [definition, in VSU_main2]
STACK [definition, in VSU_stack]
stack [definition, in VSU_stack]
stack [definition, in Verif_triang]
STACK [definition, in VSU_main]
stack [definition, in Verif_stack]
StackAPD [record, in Spec_stack]
StackASI [definition, in Spec_stack]
StackASI [section, in Spec_stack]
StackASI.M [variable, in Spec_stack]
StackASI.STACK [variable, in Spec_stack]
stackrep [projection, in Spec_stack]
stackrep_valid_pointer [projection, in Spec_stack]
stackrep_local_facts [projection, in Spec_stack]
stackrep_nil [axiom, in VSU_triang]
stacktriangVSU [lemma, in VSU_main2]
stacktriangVSU [definition, in VSU_main]
stacktriangVSU1 [definition, in VSU_main2]
stacktriangVSU1 [definition, in VSU_main]
StackVSU [lemma, in VSU_stack]
stackVSU [definition, in VSU_main]
Stack_Vprog [definition, in VSU_stack]
Stack_Gprog [definition, in VSU_stack]
Stack_internals [definition, in VSU_stack]
Stack_private [definition, in VSU_stack]
Stack_imports [definition, in VSU_stack]
stack_valid_pointer [lemma, in VSU_stack]
stack_local_prop [lemma, in VSU_stack]
Stack_VSU.M [variable, in VSU_stack]
Stack_VSU [section, in VSU_stack]
stack_valid_pointer [lemma, in Verif_triang]
stack_local_prop [lemma, in Verif_triang]
stack_valid_pointer [lemma, in Verif_stack]
stack_local_prop [lemma, in Verif_stack]
strcmp_spec [definition, in Verif_hash]
strcmp_spec [definition, in Verif_strlib]
strcpy_spec [definition, in Verif_hash]
strcpy_else_clause [lemma, in Verif_strlib]
strcpy_then_clause [lemma, in Verif_strlib]
strcpy_spec [definition, in Verif_strlib]
StringDemo [section, in Verif_strlib]
StringDemo.p [variable, in Verif_strlib]
stringlit_1_contents [definition, in Verif_strlib]
string_to_list_byte [definition, in Verif_strlib]
strlen_spec [definition, in Verif_hash]
strlen_spec [definition, in Verif_strlib]
struct_list_valid_pointer_example [lemma, in Verif_reverse]
str1:1 [binder, in Verif_hash]
str1:35 [binder, in Verif_strlib]
str1:41 [binder, in Verif_strlib]
str1:5 [binder, in Verif_hash]
str2:3 [binder, in Verif_hash]
str2:37 [binder, in Verif_strlib]
str2:43 [binder, in Verif_strlib]
str2:7 [binder, in Verif_hash]
str:17 [binder, in Verif_strlib]
str:19 [binder, in Verif_hash]
str:20 [binder, in Verif_strlib]
str:21 [binder, in Verif_hash]
st:3 [binder, in VSU_triang]
st:73 [binder, in Verif_triang]
st:76 [binder, in Verif_triang]
st:79 [binder, in Verif_triang]
st:82 [binder, in Verif_triang]
sumarray_spec [definition, in Verif_sumarray]
sum_Z_app [lemma, in Verif_sumarray]
sum_Z [definition, in Verif_sumarray]
surely_malloc_spec [definition, in VSU_stack]
sz:14 [binder, in VSU_stdlib2]
sz:17 [binder, in VSU_stdlib2]
sz:5 [binder, in Spec_stdlib]
sz:9 [binder, in Spec_stdlib]
s1a:32 [binder, in Verif_append2]
s1a:37 [binder, in Verif_append2]
s1a:53 [binder, in Verif_append1]
s1a:58 [binder, in Verif_append1]
s1c:34 [binder, in Verif_append2]
s1c:39 [binder, in Verif_append2]
s1c:55 [binder, in Verif_append1]
s1c:60 [binder, in Verif_append1]
s1:101 [binder, in Verif_append1]
s1:12 [binder, in Verif_append1]
s1:2 [binder, in Verif_hash]
s1:20 [binder, in Verif_append2]
s1:28 [binder, in Verif_append2]
s1:30 [binder, in Verif_reverse]
s1:33 [binder, in Verif_append1]
s1:34 [binder, in Verif_reverse]
s1:36 [binder, in Verif_strlib]
s1:38 [binder, in Verif_append1]
s1:42 [binder, in Verif_strlib]
s1:52 [binder, in Verif_reverse]
s1:6 [binder, in Verif_hash]
s1:62 [binder, in Verif_append2]
s1:67 [binder, in Verif_append2]
s1:69 [binder, in Verif_append1]
s1:74 [binder, in Verif_append1]
s1:8 [binder, in Verif_append1]
s1:94 [binder, in Verif_append1]
s2:102 [binder, in Verif_append1]
s2:13 [binder, in Verif_append1]
s2:21 [binder, in Verif_append2]
s2:29 [binder, in Verif_append2]
s2:31 [binder, in Verif_reverse]
s2:34 [binder, in Verif_append1]
s2:35 [binder, in Verif_reverse]
s2:38 [binder, in Verif_strlib]
s2:39 [binder, in Verif_append1]
s2:4 [binder, in Verif_hash]
s2:44 [binder, in Verif_strlib]
s2:63 [binder, in Verif_append2]
s2:68 [binder, in Verif_append2]
s2:70 [binder, in Verif_append1]
s2:75 [binder, in Verif_append1]
s2:8 [binder, in Verif_hash]
s2:9 [binder, in Verif_append1]
s2:95 [binder, in Verif_append1]
s:1 [binder, in Verif_strlib]
s:10 [binder, in Hashfun]
s:100 [binder, in Verif_hash]
s:104 [binder, in Verif_hash]
s:109 [binder, in Verif_hash]
s:114 [binder, in Verif_hash]
s:119 [binder, in Verif_hash]
s:13 [binder, in Verif_hash]
s:14 [binder, in Hashfun]
s:16 [binder, in Verif_strlib]
s:16 [binder, in Hashfun]
s:17 [binder, in Verif_hash]
s:18 [binder, in Verif_hash]
s:19 [binder, in Verif_strlib]
s:2 [binder, in Hashfun]
s:20 [binder, in Verif_hash]
s:20 [binder, in Hashfun]
s:22 [binder, in Verif_hash]
s:25 [binder, in Verif_hash]
s:26 [binder, in Verif_strlib]
s:29 [binder, in Verif_hash]
s:31 [binder, in Verif_hash]
s:32 [binder, in Verif_strlib]
s:5 [binder, in Hashfun]
s:53 [binder, in Verif_strlib]
s:57 [binder, in Verif_strlib]
s:6 [binder, in Hashfun]
s:60 [binder, in Hashfun]
s:63 [binder, in Verif_append1]
s:65 [binder, in Verif_append1]
s:67 [binder, in Verif_append1]
s:71 [binder, in Verif_append2]
s:74 [binder, in Verif_append2]
s:76 [binder, in Verif_append2]
s:78 [binder, in Verif_append2]
s:83 [binder, in Verif_hash]
s:88 [binder, in Verif_hash]
s:96 [binder, in Verif_hash]
T
table:176 [binder, in Verif_hash]table:179 [binder, in Verif_hash]
tail:18 [binder, in Verif_append2]
tail:60 [binder, in Verif_append2]
tbl:64 [binder, in Hashfun]
tbl:66 [binder, in Hashfun]
tcell [definition, in Verif_hash]
tcell [definition, in VSU_stdlib2]
thashtable [definition, in Verif_hash]
TriangASI [definition, in Spec_triang]
TriangASI [section, in Spec_triang]
TriangASI.M [variable, in Spec_triang]
TriangVSU [definition, in VSU_triang]
triangVSU [definition, in VSU_main]
triang_spec [definition, in Spec_triang]
Triang_Vprog [definition, in VSU_triang]
Triang_Gprog [definition, in VSU_triang]
Triang_internals [definition, in VSU_triang]
Triang_imports [definition, in VSU_triang]
Triang_private [definition, in VSU_triang]
Triang_VSU.STACK [variable, in VSU_triang]
Triang_VSU.M [variable, in VSU_triang]
Triang_VSU [section, in VSU_triang]
t_list_box [definition, in Verif_append2]
t_list [definition, in Verif_append1]
t_list [definition, in Verif_reverse]
t:1 [binder, in Verif_stack]
t:18 [binder, in VSU_stack]
t:20 [binder, in VSU_stack]
t:29 [binder, in Spec_stdlib]
t:3 [binder, in Verif_stack]
t:34 [binder, in Spec_stdlib]
t:35 [binder, in Verif_append2]
t:39 [binder, in Spec_stdlib]
t:40 [binder, in Verif_append2]
t:40 [binder, in Hashfun]
t:43 [binder, in Spec_stdlib]
t:44 [binder, in Hashfun]
t:48 [binder, in Hashfun]
t:49 [binder, in Spec_stdlib]
t:50 [binder, in Hashfun]
t:54 [binder, in Hashfun]
t:56 [binder, in Spec_stdlib]
t:56 [binder, in Verif_append1]
t:57 [binder, in Hashfun]
t:59 [binder, in Spec_stdlib]
t:6 [binder, in Verif_stack]
t:61 [binder, in Verif_append1]
t:69 [binder, in Hashfun]
t:72 [binder, in Hashfun]
t:9 [binder, in Verif_stack]
U
uncurry [definition, in Verif_hash]Unnamed_thm6 [definition, in Verif_hash]
Unnamed_thm5 [definition, in Verif_hash]
Unnamed_thm4 [definition, in Verif_hash]
Unnamed_thm3 [definition, in Verif_hash]
Unnamed_thm2 [definition, in Verif_hash]
Unnamed_thm1 [definition, in Verif_hash]
Unnamed_thm0 [definition, in Verif_hash]
Unnamed_thm [definition, in Verif_hash]
Unnamed_thm [definition, in Verif_sumarray]
Unnamed_thm0 [definition, in Verif_strlib]
Unnamed_thm [definition, in Verif_strlib]
Unnamed_thm [definition, in Preface]
Unnamed_thm [definition, in Preface]
u:100 [binder, in Verif_append1]
u:36 [binder, in Verif_append2]
u:41 [binder, in Verif_append2]
u:57 [binder, in Verif_append1]
u:62 [binder, in Verif_append1]
V
Verif_append1 [library]Verif_triang [library]
Verif_sumarray [library]
Verif_stack [library]
Verif_hash [library]
Verif_append2 [library]
Verif_reverse [library]
Verif_strlib [library]
Vprog [definition, in Verif_hash]
Vprog [definition, in VSU_main2]
Vprog [definition, in Verif_triang]
Vprog [definition, in Verif_append1]
Vprog [definition, in Verif_sumarray]
Vprog [definition, in Verif_reverse]
Vprog [definition, in VSU_main]
Vprog [definition, in Verif_strlib]
Vprog [definition, in Verif_stack]
VSU_stdlib [library]
VSU_stack [library]
VSU_stdlib2 [library]
VSU_intro [library]
VSU_triang [library]
VSU_main2 [library]
VSU_main [library]
v:30 [binder, in Spec_stdlib]
v:33 [binder, in Verif_reverse]
v:37 [binder, in Verif_reverse]
v:56 [binder, in Verif_reverse]
W
wandQ_frame_ver_mpred [lemma, in Verif_append2]wandQ_frame_elim_mpred [lemma, in Verif_append2]
wand_frame_ver_from_adjoint_and_modus_ponens [lemma, in Verif_append2]
wand_derives_from_adjoint_and_modus_ponens [lemma, in Verif_append2]
wand_trivial [lemma, in Verif_append2]
WholeComp [lemma, in VSU_main2]
WholeComp [lemma, in VSU_main]
WholeProgSafe [lemma, in VSU_main2]
WholeProgSafe [lemma, in VSU_main]
whole_prog [definition, in VSU_main2]
whole_prog [definition, in VSU_main]
wlseg [definition, in Verif_append2]
wlseg_weird [lemma, in Verif_append2]
wlseg_listrep_equiv [lemma, in Verif_append2]
wlseg_nullval [lemma, in Verif_append2]
wlseg_list [lemma, in Verif_append2]
wlseg_wlseg [lemma, in Verif_append2]
wlseg2lseg_nullval [lemma, in Verif_append2]
wsh:21 [binder, in Verif_strlib]
wsh:27 [binder, in Verif_strlib]
wsh:50 [binder, in Verif_strlib]
wsh:54 [binder, in Verif_strlib]
w:32 [binder, in Verif_reverse]
w:36 [binder, in Verif_reverse]
w:55 [binder, in Verif_reverse]
X
xy:72 [binder, in Verif_hash]x:10 [binder, in Verif_append1]
x:103 [binder, in Verif_append1]
x:16 [binder, in Verif_append2]
x:16 [binder, in Verif_append1]
x:165 [binder, in Verif_hash]
x:17 [binder, in VSU_stdlib]
x:17 [binder, in Verif_sumarray]
x:19 [binder, in Verif_append2]
x:22 [binder, in Verif_append2]
x:22 [binder, in Verif_append1]
x:26 [binder, in Verif_append2]
x:26 [binder, in Verif_append1]
x:30 [binder, in Verif_append2]
x:31 [binder, in Verif_append1]
x:35 [binder, in Verif_append1]
x:40 [binder, in Verif_append1]
x:40 [binder, in Verif_reverse]
x:46 [binder, in Verif_append2]
x:46 [binder, in Verif_reverse]
x:47 [binder, in Verif_append1]
x:49 [binder, in Verif_append1]
x:51 [binder, in Verif_append2]
x:52 [binder, in Verif_hash]
x:52 [binder, in Verif_append2]
x:53 [binder, in Verif_append2]
x:55 [binder, in Verif_append2]
x:58 [binder, in Verif_append2]
x:6 [binder, in Verif_append1]
x:61 [binder, in Verif_append2]
x:64 [binder, in Verif_append2]
x:64 [binder, in Verif_append1]
x:66 [binder, in Verif_append1]
x:68 [binder, in Verif_append1]
x:69 [binder, in Verif_append2]
x:7 [binder, in Verif_sumarray]
x:71 [binder, in Verif_append1]
x:72 [binder, in Verif_append2]
x:75 [binder, in Verif_append2]
x:76 [binder, in Verif_append1]
x:77 [binder, in Verif_append2]
x:79 [binder, in Verif_append2]
x:80 [binder, in Verif_append1]
x:81 [binder, in Verif_append2]
x:87 [binder, in Verif_append1]
x:91 [binder, in Verif_append1]
x:97 [binder, in Verif_append1]
Y
y:10 [binder, in Verif_reverse]y:104 [binder, in Verif_append1]
y:11 [binder, in Verif_append1]
y:16 [binder, in Verif_stack]
y:166 [binder, in Verif_hash]
y:17 [binder, in Verif_append2]
y:19 [binder, in Verif_reverse]
y:20 [binder, in Verif_append1]
y:23 [binder, in Verif_append2]
y:23 [binder, in Verif_append1]
y:27 [binder, in Verif_append2]
y:27 [binder, in Verif_append1]
y:31 [binder, in Verif_append2]
y:32 [binder, in Verif_append1]
y:36 [binder, in Verif_append1]
y:41 [binder, in Verif_append1]
y:42 [binder, in Verif_triang]
y:42 [binder, in Verif_reverse]
y:47 [binder, in Verif_reverse]
y:5 [binder, in VSU_stdlib2]
y:5 [binder, in Verif_append1]
y:5 [binder, in Verif_reverse]
y:52 [binder, in Verif_append1]
y:55 [binder, in Verif_hash]
y:56 [binder, in Verif_append2]
y:59 [binder, in Verif_append2]
y:59 [binder, in Verif_reverse]
y:6 [binder, in VSU_stack]
y:65 [binder, in Verif_append2]
y:7 [binder, in Verif_append1]
y:7 [binder, in Verif_reverse]
y:70 [binder, in Verif_append2]
y:73 [binder, in Verif_append2]
y:73 [binder, in Verif_append1]
y:77 [binder, in Verif_append1]
y:82 [binder, in Verif_append2]
y:84 [binder, in Verif_append1]
y:88 [binder, in Verif_append1]
y:92 [binder, in Verif_append1]
y:98 [binder, in Verif_append1]
Z
Zinduction [lemma, in Verif_triang]Zlength_hashtable_incr [lemma, in Hashfun]
Z_sub_add_ok [lemma, in Verif_triang]
z:167 [binder, in Verif_hash]
z:169 [binder, in Verif_hash]
z:17 [binder, in Verif_append1]
z:171 [binder, in Verif_hash]
z:173 [binder, in Verif_hash]
z:175 [binder, in Verif_hash]
z:24 [binder, in Verif_append2]
z:37 [binder, in Verif_append1]
z:43 [binder, in Verif_reverse]
z:48 [binder, in Verif_reverse]
z:66 [binder, in Verif_append2]
z:72 [binder, in Verif_append1]
z:78 [binder, in Verif_append1]
z:81 [binder, in Verif_append1]
z:93 [binder, in Verif_append1]
z:99 [binder, in Verif_append1]
Binder Index
A
al:103 [in Verif_hash]al:108 [in Verif_hash]
al:11 [in Hashfun]
al:126 [in Verif_hash]
al:130 [in Verif_hash]
al:131 [in Verif_hash]
al:139 [in Verif_hash]
al:144 [in Verif_hash]
al:178 [in Verif_hash]
al:19 [in Hashfun]
al:64 [in Verif_hash]
al:65 [in Verif_hash]
al:7 [in Hashfun]
al:87 [in Verif_triang]
a:1 [in Verif_triang]
a:1 [in Verif_sumarray]
A:123 [in Verif_hash]
a:21 [in Verif_append1]
a:24 [in Verif_append1]
a:25 [in Verif_append2]
a:25 [in Hashfun]
a:28 [in Verif_append1]
a:3 [in Verif_triang]
a:3 [in Verif_sumarray]
a:38 [in Verif_reverse]
A:42 [in Verif_append2]
a:44 [in Verif_reverse]
a:45 [in Verif_append2]
A:47 [in Verif_append2]
A:68 [in Verif_hash]
a:8 [in Verif_sumarray]
a:80 [in Verif_append2]
a:86 [in Verif_append1]
a:89 [in Verif_append1]
a:96 [in Verif_append1]
B
bl:122 [in Verif_hash]bl:75 [in Verif_hash]
bl:88 [in Verif_triang]
b0:142 [in Verif_hash]
b:148 [in Verif_hash]
b:150 [in Verif_hash]
b:2 [in Verif_triang]
b:2 [in Verif_sumarray]
b:25 [in Verif_append1]
b:29 [in Verif_append1]
b:33 [in Verif_append2]
b:38 [in Verif_append2]
b:39 [in Verif_reverse]
b:4 [in Verif_triang]
b:45 [in Verif_reverse]
b:54 [in Verif_append1]
b:59 [in Verif_append1]
B:69 [in Verif_hash]
b:90 [in Verif_append1]
C
contents:10 [in Verif_sumarray]contents:11 [in Verif_strlib]
contents:113 [in Verif_hash]
contents:118 [in Verif_hash]
contents:15 [in Verif_append2]
contents:15 [in Verif_append1]
contents:15 [in Hashfun]
contents:17 [in Hashfun]
contents:30 [in Verif_hash]
contents:32 [in Verif_hash]
contents:46 [in Verif_append1]
contents:48 [in Verif_append1]
contents:5 [in Verif_sumarray]
contents:54 [in Verif_append2]
contents:57 [in Verif_append2]
contents:6 [in Verif_strlib]
contents:73 [in Verif_hash]
contents:76 [in Verif_hash]
contents:78 [in Verif_hash]
contents:79 [in Verif_append1]
contents:85 [in Verif_append1]
contents:95 [in Verif_hash]
contents:99 [in Verif_hash]
count:133 [in Verif_hash]
count:138 [in Verif_hash]
count:155 [in Verif_hash]
count:161 [in Verif_hash]
count:34 [in Verif_hash]
count:39 [in Verif_hash]
count:43 [in Verif_hash]
count:48 [in Verif_hash]
count:61 [in Verif_hash]
count:85 [in Verif_hash]
count:90 [in Verif_hash]
cs:12 [in VSU_stdlib]
cs:26 [in Spec_stdlib]
cs:31 [in Spec_stdlib]
cs:36 [in Spec_stdlib]
cs:42 [in Spec_stdlib]
cs:48 [in Spec_stdlib]
cs:5 [in VSU_stdlib]
cs:55 [in Spec_stdlib]
cs:58 [in Spec_stdlib]
cs:8 [in VSU_stdlib]
cts:146 [in Verif_hash]
cts:147 [in Verif_hash]
cts:180 [in Verif_hash]
cts:181 [in Verif_hash]
cts:22 [in Hashfun]
cts:24 [in Hashfun]
cts:58 [in Hashfun]
cts:62 [in Hashfun]
c:30 [in Verif_append1]
C:70 [in Verif_hash]
D
dest:10 [in Verif_hash]dest:14 [in Verif_hash]
dest:23 [in Verif_strlib]
dest:29 [in Verif_strlib]
dest:51 [in Verif_strlib]
dest:55 [in Verif_strlib]
dl:157 [in Verif_hash]
dl:163 [in Verif_hash]
d:124 [in Verif_hash]
E
Espec:10 [in VSU_stdlib]Espec:4 [in VSU_stdlib]
Espec:50 [in Verif_reverse]
Espec:7 [in VSU_stdlib]
F
frees:22 [in VSU_stdlib2]f:127 [in Verif_hash]
f:16 [in Verif_sumarray]
f:71 [in Verif_hash]
G
gv:1 [in VSU_main2]gv:1 [in VSU_main]
gv:106 [in Verif_hash]
gv:11 [in Spec_stack]
gv:11 [in Verif_stack]
gv:111 [in Verif_hash]
gv:116 [in Verif_hash]
gv:12 [in Verif_sumarray]
gv:12 [in Spec_stack]
gv:121 [in Verif_hash]
gv:13 [in VSU_stdlib]
gv:13 [in Verif_sumarray]
gv:14 [in Spec_stdlib]
gv:16 [in Spec_stdlib]
gv:17 [in Spec_stack]
gv:19 [in VSU_stdlib2]
gv:19 [in VSU_stack]
gv:2 [in VSU_main2]
gv:2 [in VSU_stdlib]
gv:2 [in Spec_triang]
gv:2 [in VSU_main]
gv:2 [in Verif_stack]
gv:20 [in Spec_stdlib]
gv:21 [in VSU_stack]
gv:21 [in Spec_stack]
gv:23 [in Spec_stdlib]
gv:23 [in VSU_stdlib2]
gv:24 [in Verif_hash]
gv:25 [in Spec_stack]
gv:27 [in Verif_hash]
gv:28 [in Verif_stack]
gv:29 [in Spec_stack]
gv:29 [in Verif_stack]
gv:3 [in Spec_triang]
gv:34 [in Verif_stack]
gv:38 [in Verif_stack]
gv:4 [in Verif_stack]
gv:42 [in Verif_stack]
gv:44 [in Spec_stdlib]
gv:45 [in Spec_stdlib]
gv:46 [in Verif_stack]
gv:51 [in Spec_stdlib]
gv:53 [in Spec_stdlib]
gv:54 [in Verif_triang]
gv:55 [in Verif_triang]
gv:60 [in Verif_triang]
gv:64 [in Verif_triang]
gv:68 [in Verif_triang]
gv:72 [in Verif_triang]
gv:74 [in Verif_strlib]
gv:75 [in Verif_triang]
gv:75 [in Verif_strlib]
gv:78 [in Verif_triang]
gv:8 [in Verif_stack]
gv:80 [in Verif_hash]
gv:81 [in Verif_hash]
gv:81 [in Verif_triang]
gv:84 [in Verif_triang]
gv:85 [in Verif_triang]
gv:86 [in Verif_triang]
gv:87 [in Verif_hash]
gv:92 [in Verif_hash]
gx:14 [in VSU_stdlib]
H
hi:91 [in Verif_triang]HRE:57 [in Verif_reverse]
hs:51 [in Verif_append1]
H0:13 [in Verif_strlib]
H0:8 [in Verif_strlib]
H1:14 [in Verif_strlib]
H1:9 [in Verif_strlib]
h:1 [in Hashfun]
H:12 [in Verif_strlib]
h:177 [in Verif_hash]
h:18 [in Verif_reverse]
h:18 [in Hashfun]
h:27 [in Hashfun]
h:50 [in Verif_append1]
h:53 [in Verif_reverse]
H:58 [in Verif_reverse]
h:6 [in Verif_reverse]
H:7 [in Verif_strlib]
h:9 [in Verif_reverse]
I
il:11 [in VSU_stack]il:12 [in Verif_stack]
il:14 [in VSU_stack]
il:16 [in VSU_stack]
il:16 [in Spec_stack]
il:17 [in Verif_stack]
il:19 [in Verif_stack]
il:2 [in VSU_stack]
il:20 [in Spec_stack]
il:21 [in Verif_stack]
il:24 [in Spec_stack]
il:24 [in Verif_stack]
il:26 [in Verif_stack]
il:28 [in Spec_stack]
il:3 [in Spec_stack]
il:33 [in Verif_stack]
il:37 [in Verif_stack]
il:38 [in Verif_triang]
il:41 [in Verif_stack]
il:43 [in Verif_triang]
il:45 [in Verif_triang]
il:45 [in Verif_stack]
il:47 [in Verif_triang]
il:50 [in Verif_triang]
il:52 [in Verif_triang]
il:59 [in Verif_triang]
il:6 [in Spec_stack]
il:63 [in Verif_triang]
il:67 [in Verif_triang]
il:7 [in VSU_stack]
il:71 [in Verif_triang]
il:80 [in Verif_triang]
il:83 [in Verif_triang]
il:89 [in Verif_triang]
il:9 [in VSU_stack]
il:93 [in Verif_triang]
il:94 [in Verif_triang]
i:10 [in Verif_strlib]
i:125 [in Verif_hash]
i:14 [in Verif_sumarray]
i:15 [in Verif_sumarray]
i:15 [in Spec_stack]
i:18 [in Verif_sumarray]
i:19 [in Spec_stack]
i:20 [in VSU_stdlib2]
i:23 [in Spec_stack]
i:24 [in Spec_stdlib]
i:25 [in Spec_stdlib]
i:27 [in Spec_stack]
i:29 [in Hashfun]
i:31 [in Hashfun]
i:32 [in Verif_stack]
i:34 [in Verif_triang]
i:36 [in Verif_stack]
i:40 [in Verif_stack]
i:44 [in Verif_stack]
i:45 [in Verif_strlib]
i:46 [in Verif_strlib]
i:47 [in Verif_strlib]
i:5 [in Verif_strlib]
i:58 [in Verif_triang]
i:58 [in Verif_strlib]
i:59 [in Verif_strlib]
i:59 [in Hashfun]
i:62 [in Verif_triang]
i:63 [in Verif_strlib]
i:66 [in Verif_triang]
i:68 [in Verif_strlib]
i:70 [in Verif_triang]
i:72 [in Verif_strlib]
i:73 [in Verif_strlib]
i:9 [in Verif_hash]
i:95 [in Verif_triang]
i:96 [in Verif_triang]
i:97 [in Verif_triang]
J
j:42 [in Hashfun]j:55 [in Hashfun]
j:69 [in Verif_strlib]
j:70 [in Hashfun]
K
key:132 [in Verif_hash]key:137 [in Verif_hash]
key:154 [in Verif_hash]
key:160 [in Verif_hash]
key:33 [in Verif_hash]
key:38 [in Verif_hash]
key:42 [in Verif_hash]
key:46 [in Verif_hash]
key:60 [in Verif_hash]
key:84 [in Verif_hash]
key:89 [in Verif_hash]
kp:136 [in Verif_hash]
kp:153 [in Verif_hash]
kp:159 [in Verif_hash]
kp:37 [in Verif_hash]
kp:47 [in Verif_hash]
k':51 [in Hashfun]
k:37 [in Hashfun]
k:39 [in Hashfun]
k:43 [in Hashfun]
k:46 [in Hashfun]
k:47 [in Hashfun]
k:49 [in Hashfun]
k:52 [in Hashfun]
k:53 [in Hashfun]
k:56 [in Hashfun]
k:61 [in Hashfun]
k:63 [in Hashfun]
k:65 [in Hashfun]
k:67 [in Hashfun]
k:68 [in Hashfun]
k:71 [in Hashfun]
K:92 [in Verif_triang]
L
lo:28 [in Hashfun]lo:90 [in Verif_triang]
l:41 [in Verif_reverse]
l:49 [in Verif_reverse]
M
M:27 [in Spec_stdlib]M:32 [in Spec_stdlib]
M:37 [in Spec_stdlib]
M:41 [in Spec_stdlib]
M:47 [in Spec_stdlib]
M:54 [in Spec_stdlib]
M:57 [in Spec_stdlib]
N
next:35 [in Verif_hash]next:40 [in Verif_hash]
next:44 [in Verif_hash]
next:86 [in Verif_hash]
next:91 [in Verif_hash]
n:1 [in VSU_stdlib2]
n:11 [in Verif_hash]
n:11 [in VSU_stdlib2]
n:11 [in Verif_triang]
n:128 [in Verif_hash]
n:13 [in Spec_stdlib]
n:14 [in Verif_triang]
n:15 [in Verif_hash]
n:15 [in Spec_stdlib]
n:15 [in Verif_triang]
n:16 [in VSU_stdlib]
n:17 [in Verif_triang]
n:18 [in Spec_stdlib]
n:18 [in Verif_triang]
n:20 [in Verif_triang]
n:21 [in Spec_stdlib]
n:21 [in Verif_triang]
n:22 [in Verif_triang]
n:24 [in Verif_strlib]
n:30 [in Verif_strlib]
n:35 [in Verif_triang]
n:36 [in Verif_triang]
n:37 [in Verif_triang]
n:48 [in Verif_strlib]
n:49 [in Verif_strlib]
n:5 [in Verif_triang]
n:52 [in Verif_strlib]
n:56 [in Verif_strlib]
n:6 [in VSU_stdlib2]
n:60 [in Verif_strlib]
n:64 [in Verif_strlib]
n:74 [in Verif_triang]
n:77 [in Verif_triang]
n:8 [in VSU_stdlib2]
n:8 [in Verif_triang]
P
p':134 [in Verif_hash]p':49 [in Verif_hash]
p':62 [in Verif_hash]
P':9 [in Verif_append2]
p0:143 [in Verif_hash]
P:1 [in Verif_append2]
p:10 [in Spec_stdlib]
p:10 [in VSU_stack]
p:10 [in Verif_stack]
p:11 [in Verif_reverse]
p:112 [in Verif_hash]
p:117 [in Verif_hash]
P:12 [in Verif_append2]
p:12 [in VSU_stdlib2]
p:12 [in VSU_stack]
p:129 [in Verif_hash]
p:13 [in Verif_reverse]
p:13 [in Spec_stack]
p:13 [in Verif_stack]
p:135 [in Verif_hash]
p:14 [in Spec_stack]
p:141 [in Verif_hash]
p:145 [in Verif_hash]
p:149 [in Verif_hash]
p:15 [in VSU_stdlib2]
p:15 [in VSU_stack]
p:15 [in Verif_reverse]
p:151 [in Verif_hash]
p:152 [in Verif_hash]
p:158 [in Verif_hash]
p:164 [in Verif_hash]
p:168 [in Verif_hash]
p:17 [in Spec_stdlib]
p:17 [in VSU_stack]
p:17 [in Verif_reverse]
p:170 [in Verif_hash]
p:172 [in Verif_hash]
p:174 [in Verif_hash]
p:18 [in VSU_stdlib2]
p:18 [in Spec_stack]
p:18 [in Verif_stack]
p:19 [in Spec_stdlib]
p:2 [in VSU_stdlib2]
p:2 [in Verif_append1]
p:2 [in Verif_reverse]
p:20 [in Verif_reverse]
p:20 [in Verif_stack]
p:21 [in VSU_stdlib2]
p:22 [in Spec_stdlib]
p:22 [in VSU_stack]
p:22 [in Verif_reverse]
p:22 [in Spec_stack]
p:22 [in Verif_stack]
p:24 [in Verif_reverse]
p:25 [in Verif_stack]
p:26 [in Verif_reverse]
p:26 [in Spec_stack]
p:27 [in Verif_stack]
p:28 [in Verif_hash]
p:28 [in Verif_reverse]
p:3 [in VSU_stack]
p:30 [in Verif_stack]
p:31 [in Verif_stack]
P:33 [in Verif_triang]
p:35 [in Spec_stdlib]
p:35 [in Verif_stack]
p:36 [in Verif_hash]
p:39 [in Verif_triang]
p:39 [in Verif_stack]
P:4 [in Verif_append2]
p:4 [in Spec_stack]
p:40 [in Spec_stdlib]
p:41 [in Verif_hash]
P:43 [in Verif_append2]
p:43 [in Verif_append1]
p:43 [in Verif_stack]
p:44 [in Verif_triang]
p:45 [in Verif_hash]
p:45 [in Verif_append1]
p:46 [in Spec_stdlib]
p:46 [in Verif_triang]
P:48 [in Verif_append2]
p:48 [in Verif_triang]
p:5 [in Verif_stack]
p:50 [in Verif_hash]
p:50 [in Spec_stdlib]
p:51 [in Verif_triang]
p:52 [in Spec_stdlib]
p:53 [in Verif_triang]
p:56 [in Verif_triang]
p:57 [in Verif_hash]
p:57 [in Verif_triang]
p:59 [in Verif_hash]
P:6 [in Verif_append2]
p:6 [in Spec_stdlib]
p:61 [in Verif_triang]
p:62 [in Verif_strlib]
p:63 [in Verif_hash]
p:65 [in Verif_triang]
p:66 [in Verif_strlib]
p:67 [in Verif_hash]
p:69 [in Verif_triang]
p:7 [in VSU_stdlib2]
p:7 [in Spec_stack]
p:7 [in Verif_stack]
p:70 [in Verif_strlib]
p:74 [in Verif_hash]
p:77 [in Verif_hash]
p:79 [in Verif_hash]
P:8 [in Verif_append2]
p:8 [in VSU_stack]
p:8 [in Verif_reverse]
p:82 [in Verif_hash]
p:9 [in VSU_stdlib2]
p:93 [in Verif_hash]
p:94 [in Verif_hash]
p:98 [in Verif_hash]
Q
Q':11 [in Verif_append2]Q:10 [in Verif_append2]
Q:13 [in Verif_append2]
q:13 [in VSU_stack]
q:140 [in Verif_hash]
Q:2 [in Verif_append2]
q:23 [in Verif_stack]
q:29 [in Verif_reverse]
Q:44 [in Verif_append2]
Q:49 [in Verif_append2]
q:49 [in Verif_triang]
Q:5 [in Verif_append2]
Q:7 [in Verif_append2]
q:71 [in Verif_strlib]
R
ret:15 [in VSU_stdlib]rsh:22 [in Verif_strlib]
rsh:28 [in Verif_strlib]
r0:102 [in Verif_hash]
r0:107 [in Verif_hash]
R:14 [in Verif_append2]
r:14 [in Verif_append1]
r:156 [in Verif_hash]
r:162 [in Verif_hash]
R:3 [in Verif_append2]
R:50 [in Verif_append2]
r:54 [in Verif_reverse]
r:66 [in Verif_hash]
S
sh1:33 [in Verif_strlib]sh1:39 [in Verif_strlib]
sh2:34 [in Verif_strlib]
sh2:40 [in Verif_strlib]
sh:10 [in VSU_stdlib2]
sh:13 [in VSU_stdlib2]
sh:15 [in Verif_strlib]
sh:16 [in VSU_stdlib2]
sh:18 [in Verif_strlib]
sh:28 [in Spec_stdlib]
sh:33 [in Spec_stdlib]
sh:38 [in Spec_stdlib]
sh:4 [in Spec_stdlib]
sh:4 [in Verif_sumarray]
sh:61 [in Verif_strlib]
sh:65 [in Verif_strlib]
sh:67 [in Verif_strlib]
sh:8 [in Spec_stdlib]
sh:9 [in Verif_sumarray]
sigma:1 [in Verif_append1]
sigma:1 [in Verif_reverse]
sigma:101 [in Verif_hash]
sigma:105 [in Verif_hash]
sigma:110 [in Verif_hash]
sigma:115 [in Verif_hash]
sigma:12 [in Verif_reverse]
sigma:120 [in Verif_hash]
sigma:14 [in Verif_reverse]
sigma:16 [in Verif_reverse]
sigma:21 [in Verif_reverse]
sigma:21 [in Hashfun]
sigma:23 [in Verif_hash]
sigma:23 [in Verif_reverse]
sigma:23 [in Hashfun]
sigma:25 [in Verif_reverse]
sigma:26 [in Verif_hash]
sigma:26 [in Hashfun]
sigma:27 [in Verif_reverse]
sigma:30 [in Hashfun]
sigma:42 [in Verif_append1]
sigma:44 [in Verif_append1]
sigma:51 [in Verif_hash]
sigma:51 [in Verif_reverse]
sigma:56 [in Verif_hash]
sigma:58 [in Verif_hash]
sigma:97 [in Verif_hash]
size:11 [in Verif_sumarray]
size:6 [in Verif_sumarray]
src:12 [in Verif_hash]
src:16 [in Verif_hash]
src:25 [in Verif_strlib]
src:31 [in Verif_strlib]
str1:1 [in Verif_hash]
str1:35 [in Verif_strlib]
str1:41 [in Verif_strlib]
str1:5 [in Verif_hash]
str2:3 [in Verif_hash]
str2:37 [in Verif_strlib]
str2:43 [in Verif_strlib]
str2:7 [in Verif_hash]
str:17 [in Verif_strlib]
str:19 [in Verif_hash]
str:20 [in Verif_strlib]
str:21 [in Verif_hash]
st:3 [in VSU_triang]
st:73 [in Verif_triang]
st:76 [in Verif_triang]
st:79 [in Verif_triang]
st:82 [in Verif_triang]
sz:14 [in VSU_stdlib2]
sz:17 [in VSU_stdlib2]
sz:5 [in Spec_stdlib]
sz:9 [in Spec_stdlib]
s1a:32 [in Verif_append2]
s1a:37 [in Verif_append2]
s1a:53 [in Verif_append1]
s1a:58 [in Verif_append1]
s1c:34 [in Verif_append2]
s1c:39 [in Verif_append2]
s1c:55 [in Verif_append1]
s1c:60 [in Verif_append1]
s1:101 [in Verif_append1]
s1:12 [in Verif_append1]
s1:2 [in Verif_hash]
s1:20 [in Verif_append2]
s1:28 [in Verif_append2]
s1:30 [in Verif_reverse]
s1:33 [in Verif_append1]
s1:34 [in Verif_reverse]
s1:36 [in Verif_strlib]
s1:38 [in Verif_append1]
s1:42 [in Verif_strlib]
s1:52 [in Verif_reverse]
s1:6 [in Verif_hash]
s1:62 [in Verif_append2]
s1:67 [in Verif_append2]
s1:69 [in Verif_append1]
s1:74 [in Verif_append1]
s1:8 [in Verif_append1]
s1:94 [in Verif_append1]
s2:102 [in Verif_append1]
s2:13 [in Verif_append1]
s2:21 [in Verif_append2]
s2:29 [in Verif_append2]
s2:31 [in Verif_reverse]
s2:34 [in Verif_append1]
s2:35 [in Verif_reverse]
s2:38 [in Verif_strlib]
s2:39 [in Verif_append1]
s2:4 [in Verif_hash]
s2:44 [in Verif_strlib]
s2:63 [in Verif_append2]
s2:68 [in Verif_append2]
s2:70 [in Verif_append1]
s2:75 [in Verif_append1]
s2:8 [in Verif_hash]
s2:9 [in Verif_append1]
s2:95 [in Verif_append1]
s:1 [in Verif_strlib]
s:10 [in Hashfun]
s:100 [in Verif_hash]
s:104 [in Verif_hash]
s:109 [in Verif_hash]
s:114 [in Verif_hash]
s:119 [in Verif_hash]
s:13 [in Verif_hash]
s:14 [in Hashfun]
s:16 [in Verif_strlib]
s:16 [in Hashfun]
s:17 [in Verif_hash]
s:18 [in Verif_hash]
s:19 [in Verif_strlib]
s:2 [in Hashfun]
s:20 [in Verif_hash]
s:20 [in Hashfun]
s:22 [in Verif_hash]
s:25 [in Verif_hash]
s:26 [in Verif_strlib]
s:29 [in Verif_hash]
s:31 [in Verif_hash]
s:32 [in Verif_strlib]
s:5 [in Hashfun]
s:53 [in Verif_strlib]
s:57 [in Verif_strlib]
s:6 [in Hashfun]
s:60 [in Hashfun]
s:63 [in Verif_append1]
s:65 [in Verif_append1]
s:67 [in Verif_append1]
s:71 [in Verif_append2]
s:74 [in Verif_append2]
s:76 [in Verif_append2]
s:78 [in Verif_append2]
s:83 [in Verif_hash]
s:88 [in Verif_hash]
s:96 [in Verif_hash]
T
table:176 [in Verif_hash]table:179 [in Verif_hash]
tail:18 [in Verif_append2]
tail:60 [in Verif_append2]
tbl:64 [in Hashfun]
tbl:66 [in Hashfun]
t:1 [in Verif_stack]
t:18 [in VSU_stack]
t:20 [in VSU_stack]
t:29 [in Spec_stdlib]
t:3 [in Verif_stack]
t:34 [in Spec_stdlib]
t:35 [in Verif_append2]
t:39 [in Spec_stdlib]
t:40 [in Verif_append2]
t:40 [in Hashfun]
t:43 [in Spec_stdlib]
t:44 [in Hashfun]
t:48 [in Hashfun]
t:49 [in Spec_stdlib]
t:50 [in Hashfun]
t:54 [in Hashfun]
t:56 [in Spec_stdlib]
t:56 [in Verif_append1]
t:57 [in Hashfun]
t:59 [in Spec_stdlib]
t:6 [in Verif_stack]
t:61 [in Verif_append1]
t:69 [in Hashfun]
t:72 [in Hashfun]
t:9 [in Verif_stack]
U
u:100 [in Verif_append1]u:36 [in Verif_append2]
u:41 [in Verif_append2]
u:57 [in Verif_append1]
u:62 [in Verif_append1]
V
v:30 [in Spec_stdlib]v:33 [in Verif_reverse]
v:37 [in Verif_reverse]
v:56 [in Verif_reverse]
W
wsh:21 [in Verif_strlib]wsh:27 [in Verif_strlib]
wsh:50 [in Verif_strlib]
wsh:54 [in Verif_strlib]
w:32 [in Verif_reverse]
w:36 [in Verif_reverse]
w:55 [in Verif_reverse]
X
xy:72 [in Verif_hash]x:10 [in Verif_append1]
x:103 [in Verif_append1]
x:16 [in Verif_append2]
x:16 [in Verif_append1]
x:165 [in Verif_hash]
x:17 [in VSU_stdlib]
x:17 [in Verif_sumarray]
x:19 [in Verif_append2]
x:22 [in Verif_append2]
x:22 [in Verif_append1]
x:26 [in Verif_append2]
x:26 [in Verif_append1]
x:30 [in Verif_append2]
x:31 [in Verif_append1]
x:35 [in Verif_append1]
x:40 [in Verif_append1]
x:40 [in Verif_reverse]
x:46 [in Verif_append2]
x:46 [in Verif_reverse]
x:47 [in Verif_append1]
x:49 [in Verif_append1]
x:51 [in Verif_append2]
x:52 [in Verif_hash]
x:52 [in Verif_append2]
x:53 [in Verif_append2]
x:55 [in Verif_append2]
x:58 [in Verif_append2]
x:6 [in Verif_append1]
x:61 [in Verif_append2]
x:64 [in Verif_append2]
x:64 [in Verif_append1]
x:66 [in Verif_append1]
x:68 [in Verif_append1]
x:69 [in Verif_append2]
x:7 [in Verif_sumarray]
x:71 [in Verif_append1]
x:72 [in Verif_append2]
x:75 [in Verif_append2]
x:76 [in Verif_append1]
x:77 [in Verif_append2]
x:79 [in Verif_append2]
x:80 [in Verif_append1]
x:81 [in Verif_append2]
x:87 [in Verif_append1]
x:91 [in Verif_append1]
x:97 [in Verif_append1]
Y
y:10 [in Verif_reverse]y:104 [in Verif_append1]
y:11 [in Verif_append1]
y:16 [in Verif_stack]
y:166 [in Verif_hash]
y:17 [in Verif_append2]
y:19 [in Verif_reverse]
y:20 [in Verif_append1]
y:23 [in Verif_append2]
y:23 [in Verif_append1]
y:27 [in Verif_append2]
y:27 [in Verif_append1]
y:31 [in Verif_append2]
y:32 [in Verif_append1]
y:36 [in Verif_append1]
y:41 [in Verif_append1]
y:42 [in Verif_triang]
y:42 [in Verif_reverse]
y:47 [in Verif_reverse]
y:5 [in VSU_stdlib2]
y:5 [in Verif_append1]
y:5 [in Verif_reverse]
y:52 [in Verif_append1]
y:55 [in Verif_hash]
y:56 [in Verif_append2]
y:59 [in Verif_append2]
y:59 [in Verif_reverse]
y:6 [in VSU_stack]
y:65 [in Verif_append2]
y:7 [in Verif_append1]
y:7 [in Verif_reverse]
y:70 [in Verif_append2]
y:73 [in Verif_append2]
y:73 [in Verif_append1]
y:77 [in Verif_append1]
y:82 [in Verif_append2]
y:84 [in Verif_append1]
y:88 [in Verif_append1]
y:92 [in Verif_append1]
y:98 [in Verif_append1]
Z
z:167 [in Verif_hash]z:169 [in Verif_hash]
z:17 [in Verif_append1]
z:171 [in Verif_hash]
z:173 [in Verif_hash]
z:175 [in Verif_hash]
z:24 [in Verif_append2]
z:37 [in Verif_append1]
z:43 [in Verif_reverse]
z:48 [in Verif_reverse]
z:66 [in Verif_append2]
z:72 [in Verif_append1]
z:78 [in Verif_append1]
z:81 [in Verif_append1]
z:93 [in Verif_append1]
z:99 [in Verif_append1]
Module Index
C
COUNT_TABLE [in Hashfun]D
Digression [in VSU_stdlib2]F
FunTable [in Hashfun]I
IntHashTable [in Hashfun]Variable Index
M
MallocFreeASI.M [in Spec_stdlib]S
StackASI.M [in Spec_stack]StackASI.STACK [in Spec_stack]
Stack_VSU.M [in VSU_stack]
StringDemo.p [in Verif_strlib]
T
TriangASI.M [in Spec_triang]Triang_VSU.STACK [in VSU_triang]
Triang_VSU.M [in VSU_triang]
Library Index
B
BibH
HashfunP
PostscriptPreface
S
Spec_stdlibSpec_stack
Spec_triang
V
Verif_append1Verif_triang
Verif_sumarray
Verif_stack
Verif_hash
Verif_append2
Verif_reverse
Verif_strlib
VSU_stdlib
VSU_stack
VSU_stdlib2
VSU_intro
VSU_triang
VSU_main2
VSU_main
Lemma Index
A
add_another [in Verif_triang]add_list_sublist_bounds [in Verif_triang]
add_list_nonneg [in Verif_triang]
add_list_app [in Verif_triang]
add_list_decreasing_eq [in Verif_triang]
add_list_decreasing_eq_alt [in Verif_triang]
B
body_incr [in Verif_hash]body_incr_field_address_lemma [in Verif_hash]
body_incr_list [in Verif_hash]
body_get [in Verif_hash]
body_new_table [in Verif_hash]
body_new_table_helper [in Verif_hash]
body_new_cell [in Verif_hash]
body_copy_string [in Verif_hash]
body_hash [in Verif_hash]
body_main [in VSU_main2]
body_append_alter2 [in Verif_append2]
body_exit [in VSU_stdlib2]
body_free [in VSU_stdlib2]
body_malloc [in VSU_stdlib2]
body_surely_malloc [in VSU_stack]
body_newstack [in VSU_stack]
body_push [in VSU_stack]
body_pop [in VSU_stack]
body_main [in Verif_triang]
body_pop_and_add [in Verif_triang]
body_pop_and_add [in Verif_triang]
body_push_increasing [in Verif_triang]
body_append_alter1 [in Verif_append1]
body_append [in Verif_append1]
body_main [in Verif_sumarray]
body_sumarray [in Verif_sumarray]
body_reverse_step [in Verif_reverse]
body_reverse [in Verif_reverse]
body_triang [in VSU_triang]
body_pop_and_add [in VSU_triang]
body_push_increasing [in VSU_triang]
body_main [in VSU_main]
body_strcmp [in Verif_strlib]
body_example_call_strcpy [in Verif_strlib]
body_strcpy [in Verif_strlib]
body_strlen [in Verif_strlib]
body_newstack [in Verif_stack]
body_push [in Verif_stack]
body_pop [in Verif_stack]
C
cancel_example [in Verif_strlib]D
data_at_thashtable_tarray [in Verif_hash]data_at_isptr_example2 [in Verif_reverse]
data_at_isptr_example1 [in Verif_reverse]
data_at_Vundef_example [in Verif_strlib]
data_at_Vundef_example [in Verif_strlib]
demonstrate_cstring2 [in Verif_strlib]
demonstrate_cstring1 [in Verif_strlib]
E
emp_lbseg [in Verif_append2]emp_wlseg [in Verif_append2]
emp_wand_emp_left [in Verif_append2]
emp_wand_emp_right [in Verif_append2]
example_field_at_data_at''' [in Verif_hash]
example_field_at_data_at'' [in Verif_hash]
example_field_at_data_at' [in Verif_hash]
example_field_at_data_at [in Verif_hash]
example_split_struct [in Verif_hash]
F
freelistrep_valid_pointer [in VSU_stdlib2]freelistrep_local_prop [in VSU_stdlib2]
free_spec_sub [in Spec_stdlib]
FunTable.gempty [in Hashfun]
FunTable.gso [in Hashfun]
FunTable.gss [in Hashfun]
H
hashfun_snoc [in Hashfun]hashfun_aux_snoc [in Hashfun]
hashfun_inrange [in Hashfun]
hashtable_rep_valid_pointer [in Verif_hash]
hashtable_rep_local_facts [in Verif_hash]
hashtable_get_unfold [in Hashfun]
I
implies_and_adjoint [in Verif_append2]initialize [in VSU_stdlib]
initialize [in VSU_stdlib2]
IntHashTable.empty_invariant [in Hashfun]
IntHashTable.gempty [in Hashfun]
IntHashTable.gso [in Hashfun]
IntHashTable.gss [in Hashfun]
IntHashTable.incr_invariant [in Hashfun]
Int_repr_eq_mod [in Hashfun]
iter_sepcon_split3 [in Verif_hash]
iter_sepcon_listrep_local_facts [in Verif_hash]
L
lbseg_lbseg [in Verif_append2]listboxrep_traverse32 [in Verif_hash]
listboxrep_traverse [in Verif_hash]
listbox_lbseg [in Verif_append2]
listcell_fold [in Verif_hash]
listrep_traverse_finish [in Verif_hash]
listrep_traverse_step_example [in Verif_hash]
listrep_traverse_step [in Verif_hash]
listrep_traverse_start [in Verif_hash]
listrep_fold [in Verif_hash]
listrep_valid_pointer [in Verif_hash]
listrep_local_prop [in Verif_hash]
listrep_valid_pointer [in VSU_stack]
listrep_local_prop [in VSU_stack]
listrep_valid_pointer [in Verif_triang]
listrep_local_prop [in Verif_triang]
listrep_nonnull [in Verif_append1]
listrep_null [in Verif_append1]
listrep_valid_pointer [in Verif_append1]
listrep_local_facts [in Verif_append1]
listrep_len_ge2_address_different [in Verif_reverse]
listrep_len_ge2_fact [in Verif_reverse]
listrep_valid_pointer [in Verif_reverse]
listrep_valid_pointer_example [in Verif_reverse]
listrep_local_facts [in Verif_reverse]
listrep_facts_example [in Verif_reverse]
listrep_facts_example [in Verif_reverse]
listrep_valid_pointer [in Verif_stack]
listrep_local_prop [in Verif_stack]
listrep2lseg [in Verif_append1]
loopy_lseg_no_connection [in Verif_append1]
loopy_lseg_not_bad [in Verif_append1]
lseg_lseg_inv [in Verif_append1]
lseg_listrep_equiv [in Verif_append1]
lseg_list [in Verif_append1]
lseg_lseg [in Verif_append1]
lseg_maybe_loop [in Verif_append1]
lseg2listrep [in Verif_append1]
lseg2wlseg [in Verif_append2]
M
malloc_spec_sub [in Spec_stdlib]malloc_token_local_facts [in Spec_stdlib]
malloc_token_valid_pointer [in Spec_stdlib]
malloc_token_sz_local_facts [in VSU_stdlib2]
malloc_token_sz_valid_pointer [in VSU_stdlib2]
modus_ponens_wand_from_adjoint [in Verif_append2]
N
nat_sub_add_yuck [in Verif_triang]nt_lseg_list [in Verif_append1]
nt_lseg_nt_lseg [in Verif_append1]
N_eq [in Hashfun]
P
prog_correct [in Verif_sumarray]S
semax_func_cons_malloc_aux [in VSU_stdlib]singleton_wlseg [in Verif_append2]
singleton_nt_lseg' [in Verif_append1]
singleton_nt_lseg [in Verif_append1]
singleton_lseg [in Verif_append1]
stacktriangVSU [in VSU_main2]
StackVSU [in VSU_stack]
stack_valid_pointer [in VSU_stack]
stack_local_prop [in VSU_stack]
stack_valid_pointer [in Verif_triang]
stack_local_prop [in Verif_triang]
stack_valid_pointer [in Verif_stack]
stack_local_prop [in Verif_stack]
strcpy_else_clause [in Verif_strlib]
strcpy_then_clause [in Verif_strlib]
struct_list_valid_pointer_example [in Verif_reverse]
sum_Z_app [in Verif_sumarray]
W
wandQ_frame_ver_mpred [in Verif_append2]wandQ_frame_elim_mpred [in Verif_append2]
wand_frame_ver_from_adjoint_and_modus_ponens [in Verif_append2]
wand_derives_from_adjoint_and_modus_ponens [in Verif_append2]
wand_trivial [in Verif_append2]
WholeComp [in VSU_main2]
WholeComp [in VSU_main]
WholeProgSafe [in VSU_main2]
WholeProgSafe [in VSU_main]
wlseg_weird [in Verif_append2]
wlseg_listrep_equiv [in Verif_append2]
wlseg_nullval [in Verif_append2]
wlseg_list [in Verif_append2]
wlseg_wlseg [in Verif_append2]
wlseg2lseg_nullval [in Verif_append2]
Z
Zinduction [in Verif_triang]Zlength_hashtable_incr [in Hashfun]
Z_sub_add_ok [in Verif_triang]
Axiom Index
B
body_exit [in VSU_stdlib]body_free [in VSU_stdlib]
body_malloc [in VSU_stdlib]
C
COUNT_TABLE.gso [in Hashfun]COUNT_TABLE.gss [in Hashfun]
COUNT_TABLE.gempty [in Hashfun]
COUNT_TABLE.incr [in Hashfun]
COUNT_TABLE.get [in Hashfun]
COUNT_TABLE.empty [in Hashfun]
COUNT_TABLE.key [in Hashfun]
COUNT_TABLE.table [in Hashfun]
M
M [in VSU_stdlib]make_mem_mgr [in VSU_stdlib]
S
stackrep_nil [in VSU_triang]Projection Index
M
malloc_token_sz_local_facts [in Spec_stdlib]malloc_token_sz_valid_pointer [in Spec_stdlib]
malloc_token_sz [in Spec_stdlib]
mem_mgr [in Spec_stdlib]
S
stackrep [in Spec_stack]stackrep_valid_pointer [in Spec_stack]
stackrep_local_facts [in Spec_stack]
Instance Index
C
CompSpecs [in Verif_hash]Compspecs [in VSU_main2]
CompSpecs [in VSU_stdlib]
CompSpecs [in VSU_stdlib2]
CompSpecs [in VSU_stack]
CompSpecs [in Verif_triang]
CompSpecs [in Verif_append1]
CompSpecs [in Verif_sumarray]
CompSpecs [in Verif_reverse]
CompSpecs [in VSU_triang]
Compspecs [in VSU_main]
CompSpecs [in VSU_main]
CompSpecs [in Verif_strlib]
CompSpecs [in Verif_stack]
E
EqDec_string [in Hashfun]Section Index
M
MallocFreeASI [in Spec_stdlib]S
StackASI [in Spec_stack]Stack_VSU [in VSU_stack]
StringDemo [in Verif_strlib]
T
TriangASI [in Spec_triang]Triang_VSU [in VSU_triang]
Definition Index
A
add_list [in Verif_triang]append_spec [in Verif_append1]
C
copy_string_spec [in Verif_hash]coreVSU [in VSU_main2]
coreVSU [in VSU_main]
D
decreasing_Z1 [in Verif_triang]decreasing_Z1_aux [in Verif_triang]
decreasing_Z [in Verif_triang]
decreasing_nat [in Verif_triang]
Digression.N [in VSU_stdlib2]
Digression.N_eq [in VSU_stdlib2]
Digression.N' [in VSU_stdlib2]
Digression.N'' [in VSU_stdlib2]
E
empty_table [in Hashfun]example_call_strcpy_spec [in Verif_strlib]
exit_spec [in Spec_stdlib]
F
four_contents [in Verif_sumarray]freelistrep [in VSU_stdlib2]
free_spec [in Spec_stdlib]
free_spec_sz [in Spec_stdlib]
free_spec_example [in Verif_stack]
FunTable.empty [in Hashfun]
FunTable.get [in Hashfun]
FunTable.incr [in Hashfun]
FunTable.key [in Hashfun]
FunTable.table [in Hashfun]
G
get_spec [in Verif_hash]Gprog [in Verif_hash]
Gprog [in Verif_triang]
Gprog [in Verif_append1]
Gprog [in Verif_sumarray]
Gprog [in Verif_reverse]
Gprog [in Verif_strlib]
Gprog [in Verif_stack]
H
hashfun [in Hashfun]hashfun_aux [in Hashfun]
hashtable_rep [in Verif_hash]
hashtable_incr [in Hashfun]
hashtable_get [in Hashfun]
hashtable_contents [in Hashfun]
hash_spec [in Verif_hash]
Hello [in Verif_strlib]
Hello' [in Verif_strlib]
I
incr_spec [in Verif_hash]incr_list_spec [in Verif_hash]
IntHashTable.empty [in Hashfun]
IntHashTable.get [in Hashfun]
IntHashTable.hashtable_invariant [in Hashfun]
IntHashTable.incr [in Hashfun]
IntHashTable.key [in Hashfun]
IntHashTable.table [in Hashfun]
L
lbseg [in Verif_append2]listboxrep [in Verif_hash]
listboxrep [in Verif_append2]
listrep [in Verif_hash]
listrep [in VSU_stack]
listrep [in Verif_triang]
listrep [in Verif_append1]
listrep [in Verif_reverse]
listrep [in Verif_stack]
list_cell_valid_pointer [in Verif_hash]
list_cell_local_facts [in Verif_hash]
list_cell [in Verif_hash]
list_incr [in Hashfun]
list_get [in Hashfun]
lseg [in Verif_append1]
M
M [in VSU_main2]M [in VSU_stdlib2]
M [in VSU_main]
MainComp [in VSU_main2]
MainComp [in VSU_main]
Main_Gprog [in VSU_main2]
Main_imports [in VSU_main2]
main_spec [in VSU_main2]
main_spec [in Verif_triang]
main_spec [in Verif_sumarray]
Main_Gprog [in VSU_main]
Main_imports [in VSU_main]
main_spec [in VSU_main]
MallocFreeASI [in Spec_stdlib]
MallocFreeVSU [in VSU_stdlib]
MallocFreeVSU [in VSU_stdlib2]
malloc_spec [in Spec_stdlib]
malloc_token [in Spec_stdlib]
malloc_spec_sz [in Spec_stdlib]
malloc_token_sz [in VSU_stdlib2]
malloc_spec_example [in Verif_stack]
mem_mgr [in VSU_stdlib2]
MFGprog [in VSU_stdlib]
MFGprog [in VSU_stdlib2]
MFVprog [in VSU_stdlib]
MFVprog [in VSU_stdlib2]
MF_E [in VSU_stdlib]
MF_globals [in VSU_stdlib]
MF_internal_specs [in VSU_stdlib]
MF_imported_specs [in VSU_stdlib]
MF_ASI [in VSU_stdlib]
MF_Externs [in VSU_stdlib2]
MF_globals [in VSU_stdlib2]
MF_internal_specs [in VSU_stdlib2]
MF_imported_specs [in VSU_stdlib2]
MF_ASI [in VSU_stdlib2]
N
N [in VSU_stdlib2]N [in Hashfun]
newstack_spec [in Verif_triang]
newstack_spec [in Spec_stack]
newstack_spec [in Verif_stack]
new_cell_spec [in Verif_hash]
new_table_spec [in Verif_hash]
nt_lseg [in Verif_append1]
N_eq [in VSU_stdlib2]
P
placeholder_spec [in VSU_stdlib]pop_and_add_spec [in Verif_triang]
pop_spec [in Verif_triang]
pop_spec [in Spec_stack]
pop_and_add_spec [in VSU_triang]
pop_spec [in Verif_stack]
push_increasing_spec [in Verif_triang]
push_spec [in Verif_triang]
push_spec [in Spec_stack]
push_increasing_spec [in VSU_triang]
push_spec [in Verif_stack]
R
release_needed [in Preface]reverse_spec [in Verif_reverse]
S
STACK [in VSU_main2]STACK [in VSU_stack]
stack [in VSU_stack]
stack [in Verif_triang]
STACK [in VSU_main]
stack [in Verif_stack]
StackASI [in Spec_stack]
stacktriangVSU [in VSU_main]
stacktriangVSU1 [in VSU_main2]
stacktriangVSU1 [in VSU_main]
stackVSU [in VSU_main]
Stack_Vprog [in VSU_stack]
Stack_Gprog [in VSU_stack]
Stack_internals [in VSU_stack]
Stack_private [in VSU_stack]
Stack_imports [in VSU_stack]
strcmp_spec [in Verif_hash]
strcmp_spec [in Verif_strlib]
strcpy_spec [in Verif_hash]
strcpy_spec [in Verif_strlib]
stringlit_1_contents [in Verif_strlib]
string_to_list_byte [in Verif_strlib]
strlen_spec [in Verif_hash]
strlen_spec [in Verif_strlib]
sumarray_spec [in Verif_sumarray]
sum_Z [in Verif_sumarray]
surely_malloc_spec [in VSU_stack]
T
tcell [in Verif_hash]tcell [in VSU_stdlib2]
thashtable [in Verif_hash]
TriangASI [in Spec_triang]
TriangVSU [in VSU_triang]
triangVSU [in VSU_main]
triang_spec [in Spec_triang]
Triang_Vprog [in VSU_triang]
Triang_Gprog [in VSU_triang]
Triang_internals [in VSU_triang]
Triang_imports [in VSU_triang]
Triang_private [in VSU_triang]
t_list_box [in Verif_append2]
t_list [in Verif_append1]
t_list [in Verif_reverse]
U
uncurry [in Verif_hash]Unnamed_thm6 [in Verif_hash]
Unnamed_thm5 [in Verif_hash]
Unnamed_thm4 [in Verif_hash]
Unnamed_thm3 [in Verif_hash]
Unnamed_thm2 [in Verif_hash]
Unnamed_thm1 [in Verif_hash]
Unnamed_thm0 [in Verif_hash]
Unnamed_thm [in Verif_hash]
Unnamed_thm [in Verif_sumarray]
Unnamed_thm0 [in Verif_strlib]
Unnamed_thm [in Verif_strlib]
Unnamed_thm [in Preface]
Unnamed_thm [in Preface]
V
Vprog [in Verif_hash]Vprog [in VSU_main2]
Vprog [in Verif_triang]
Vprog [in Verif_append1]
Vprog [in Verif_sumarray]
Vprog [in Verif_reverse]
Vprog [in VSU_main]
Vprog [in Verif_strlib]
Vprog [in Verif_stack]
W
whole_prog [in VSU_main2]whole_prog [in VSU_main]
wlseg [in Verif_append2]
Record Index
M
MallocFreeAPD [in Spec_stdlib]S
StackAPD [in Spec_stack]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1260 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (820 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (170 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (192 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
This page has been generated by coqdoc