| 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 |
_ |
(640 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 |
_ |
(4 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 |
_ |
(157 entries) |
| Constructor 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 |
_ |
(159 entries) |
| Inductive 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 |
_ |
(94 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 |
_ |
(190 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 |
_ |
(7 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 |
_ |
(29 entries) |
Global Index
A
AbDef [definition, in ObjectAlgebraImplem_struct]
AbDef_correct [lemma, in ObjectAlgebraImplem_struct]
AbDef_rec [definition, in ObjectAlgebraImplem_struct]
AbDef_rec_correct [lemma, in ObjectAlgebraImplem_struct]
AbInit [definition, in correct]
AbInit_correct [lemma, in correct]
AbMem [inductive, in correct]
AbMemOrder [inductive, in correct]
AbMemOrder_def [constructor, in correct]
AbNumConst [inductive, in NumAlgebraImplem_const]
AbNumConstjoin [definition, in NumAlgebraImplem_const]
AbNumConstLattice [definition, in NumAlgebraImplem_const]
AbNumConstOrder [inductive, in NumAlgebraImplem_const]
AbNumConstPoset [definition, in NumAlgebraImplem_const]
AbNumTop [inductive, in NumAlgebraImplem_top]
AbNumTopjoin [definition, in NumAlgebraImplem_top]
AbNumTopLattice [definition, in NumAlgebraImplem_top]
AbNumTopOrder [inductive, in NumAlgebraImplem_top]
AbNumTopPoset [definition, in NumAlgebraImplem_top]
AbState [definition, in correct]
AbstractSemantic [definition, in correct]
AbstractSemantic_correct [lemma, in correct]
AbTransfMem [definition, in correct]
AbTransfMem_correct_aux [lemma, in correct]
AbTransfPC_correct [lemma, in correct]
AbTransf_correct [lemma, in correct]
AbTransPC [definition, in correct]
accR_property_some_stack [definition, in StackLattice]
accS_property [definition, in StackLattice]
acc_property_bot [definition, in StackLattice]
acc_property_const [definition, in NumAlgebraImplem_const]
acc_property_some_stack [definition, in StackLattice]
acc_property_top [definition, in StackLattice]
acc_property_top [definition, in NumAlgebraImplem_const]
AlgebraType [library]
all [library]
applyArray [definition, in ArrayLattice]
applyArray_eq_word [lemma, in ArrayLattice]
applyArray_monotone [lemma, in ArrayLattice]
applyFunc [definition, in ArrayLattice]
applyFunc_monotone [lemma, in ArrayLattice]
apply_bottom [lemma, in ArrayLattice]
apply_build_const_TabTree_is_bot [lemma, in TabTree]
apply_build_const_TabTree_is_const [lemma, in TabTree]
apply_const [lemma, in ArrayLattice]
apply_functree [definition, in ArrayLattice]
apply_is_bottom [lemma, in ArrayLattice]
apply_join_tree [lemma, in ArrayLattice]
apply_modifyArray1 [lemma, in ArrayLattice]
apply_modifyArray2 [lemma, in ArrayLattice]
apply_modify1 [lemma, in ArrayLattice]
apply_modify2 [lemma, in ArrayLattice]
apply_modify_eq1 [lemma, in ArrayLattice]
apply_modify_eq2 [lemma, in ArrayLattice]
apply_modify_set1 [lemma, in FiniteSetLattice]
apply_modify_set2 [lemma, in FiniteSetLattice]
apply_modify_set_tree [lemma, in TabTree]
apply_modify_set_tree1 [lemma, in TabTree]
apply_modify_tree1 [lemma, in TabTree]
apply_modify_tree2 [lemma, in TabTree]
apply_monotone [lemma, in ArrayLattice]
apply_set [definition, in FiniteSetLattice]
apply_set_in [lemma, in FiniteSetLattice]
apply_set_tree [definition, in TabTree]
apply_set_tree1 [lemma, in TabTree]
apply_substArray1 [lemma, in ArrayLattice]
apply_substArray2 [lemma, in ArrayLattice]
apply_subst1 [lemma, in ArrayLattice]
apply_subst2 [lemma, in ArrayLattice]
apply_subst_eq1 [lemma, in ArrayLattice]
apply_subst_eq2 [lemma, in ArrayLattice]
apply_subst_leaf1 [lemma, in TabTree]
apply_subst_leaf2 [lemma, in TabTree]
apply_subst_tree1 [lemma, in TabTree]
apply_subst_tree2 [lemma, in TabTree]
apply_tree [definition, in TabTree]
apply_tree_bot [lemma, in ArrayLattice]
ArrayLattice [definition, in ArrayLattice]
ArrayLattice [library]
ArrayPoset [definition, in ArrayLattice]
B
betaTypeOfField [definition, in ObjectAlgebraImplem_struct]
betaTypeOfField_correct [lemma, in ObjectAlgebraImplem_struct]
BoolLattice [library]
BoolPoset [definition, in BoolLattice]
bool_order [inductive, in BoolLattice]
bot [constructor, in NumAlgebraImplem_const]
bot_order [constructor, in NumAlgebraImplem_const]
bot_stack [constructor, in StackLattice]
bot_sum [constructor, in SumLattice]
build_const_TabTree_rec [definition, in TabTree]
C
CallStack [definition, in semantic]
Class [inductive, in syntax]
ClassInst [inductive, in semantic]
ClassName [definition, in syntax]
class_substField [lemma, in semantic]
compose [inductive, in Pow]
compose1 [inductive, in rel]
compose1_def [constructor, in rel]
compose2 [inductive, in Pow]
compose2 [inductive, in rel]
compose2_def [constructor, in Pow]
compose2_def [constructor, in rel]
compose3 [inductive, in rel]
compose3_def [constructor, in rel]
compose_def [constructor, in Pow]
config [constructor, in semantic]
Connect [inductive, in AlgebraType]
Connect [inductive, in AlgebraType]
Connect [inductive, in AlgebraType]
Connect [inductive, in AlgebraType]
Connect [inductive, in AlgebraType]
Connect [inductive, in AlgebraType]
Connect [inductive, in AlgebraType]
const [constructor, in NumAlgebraImplem_const]
const [definition, in ArrayLattice]
const [inductive, in rel]
const_def [constructor, in rel]
const_order [constructor, in NumAlgebraImplem_const]
Context [definition, in semantic]
correct [library]
correct1 [definition, in Pow]
correct2 [definition, in Pow]
criterium1 [lemma, in Pow]
criterium2 [lemma, in Pow]
Ct [definition, in semantic]
currentState [definition, in semantic]
D
def [definition, in semantic]
definedFields [definition, in syntax]
definedFields_eq_word [lemma, in syntax]
def_op [inductive, in funcsem]
def_op_def [constructor, in funcsem]
E
eqS [inductive, in StackLattice]
eqS_dec [definition, in StackLattice]
eqS_refl [definition, in StackLattice]
eqS_sym [definition, in StackLattice]
eqS_trans [definition, in StackLattice]
eq' [inductive, in ArrayLattice]
eq'_dec [lemma, in ArrayLattice]
eq'_leaf [constructor, in ArrayLattice]
eq'_leaf_node [constructor, in ArrayLattice]
eq'_node_leaf [constructor, in ArrayLattice]
eq'_node_node [constructor, in ArrayLattice]
eq'_sym [lemma, in ArrayLattice]
eq'_to_Feq [lemma, in ArrayLattice]
eq'_trans [lemma, in ArrayLattice]
eq_bot_stack [constructor, in StackLattice]
eq_cons [constructor, in StackLattice]
eq_dec [definition, in Lattice]
eq_funcTree' [inductive, in ArrayLattice]
eq_funcTree'_none [constructor, in ArrayLattice]
eq_funcTree'_some [constructor, in ArrayLattice]
eq_nil [constructor, in StackLattice]
eq_order_order [lemma, in Lattice]
eq_top_stack [constructor, in StackLattice]
eq_word [definition, in PosInf]
eq_word_dec [lemma, in PosInf]
eq_word_refl [lemma, in PosInf]
eq_word_sym [lemma, in PosInf]
eq_word_trans [lemma, in PosInf]
F
false_order [constructor, in BoolLattice]
Fbottom [definition, in ArrayLattice]
Fcompose [definition, in Pow]
Fcompose2 [definition, in Pow]
Feq [definition, in ArrayLattice]
Field [inductive, in syntax]
FieldName [definition, in syntax]
fieldNum [constructor, in syntax]
fieldRef [constructor, in syntax]
fieldValue_substField1 [lemma, in semantic]
fieldValue_substField2 [lemma, in semantic]
Field_dec [definition, in syntax]
FiniteSet [definition, in FiniteSetLattice]
FiniteSetLattice [library]
fix_implies_fix_iter [lemma, in Lattice]
Fjoin [definition, in ArrayLattice]
Forder_to_order' [lemma, in ArrayLattice]
Frame [inductive, in semantic]
frame [constructor, in semantic]
FuncSem [inductive, in funcsem]
funcsem [library]
funcTree [inductive, in ArrayLattice]
funcTree' [definition, in ArrayLattice]
funcTree_Lattice [definition, in ArrayLattice]
funcTree_Poset [definition, in ArrayLattice]
f_in_listf_prop1 [lemma, in Lattice]
f_in_listf_prop2 [lemma, in Lattice]
f_in_listf_prop3 [lemma, in Lattice]
G
Gamma [inductive, in Gamma]
Gamma [library]
GammaBestTop [inductive, in Gamma]
gammaBestTopRefPt [definition, in RefAlgebraImplem_point]
gammaCl [definition, in RefAlgebraImplem_class]
gammaHeap [definition, in HeapAlgebraImplem_fs]
gammaHeap_monotone [lemma, in correct]
gammaHeap_monotone' [lemma, in correct]
gammaLocalVar1 [definition, in LocalVarAlgebraImplem_struct]
gammaLocalVar_monotone [lemma, in correct]
gammaMem [inductive, in correct]
gammaMem_def [constructor, in correct]
gammaMem_monotone [lemma, in correct]
GammaMonotone [definition, in Gamma]
GammaMonotone_incl [lemma, in Gamma]
gammaNumConst [definition, in NumAlgebraImplem_const]
gammaNumTop [definition, in NumAlgebraImplem_top]
gammaObjectPointWise [definition, in ObjectAlgebraImplem_struct]
gammaPt [definition, in RefAlgebraImplem_point]
gammaRefCl [definition, in RefAlgebraImplem_class]
gammaRefPt [definition, in RefAlgebraImplem_point]
gammaSt [inductive, in correct]
gammaStack [definition, in StackAlgebraImplem_struct]
gammaStack_monotone [lemma, in correct]
gammaSt_def [constructor, in correct]
gammaSum [inductive, in StackAlgebraImplem_struct]
gammaSum_cons [constructor, in StackAlgebraImplem_struct]
gammaSum_nil [constructor, in StackAlgebraImplem_struct]
GammaTop [inductive, in Gamma]
gammaTopBestRefCl [definition, in RefAlgebraImplem_class]
gammaTopNumConst [definition, in NumAlgebraImplem_const]
gammaTopNumTop [definition, in NumAlgebraImplem_top]
gammaTopObjectPointWise [definition, in ObjectAlgebraImplem_struct]
gammaTopRefCl [definition, in RefAlgebraImplem_class]
gammaTopRefPt [definition, in RefAlgebraImplem_point]
gammaTopValueSum [definition, in ValueAlgebraImplem_sum2]
gammaValueSum [definition, in ValueAlgebraImplem_sum2]
getfield [constructor, in syntax]
getfield1 [constructor, in semantic]
getfield1_monotone_for_gammaHeap [constructor, in semantic]
getfield_rule [constructor, in semantic]
getf_op [inductive, in funcsem]
getf_op_def [constructor, in funcsem]
getN_op [inductive, in funcsem]
getN_op_def [constructor, in funcsem]
geto_op [inductive, in funcsem]
geto_op_def [constructor, in funcsem]
getR_op [inductive, in funcsem]
getR_op_def [constructor, in funcsem]
get_op [inductive, in funcsem]
get_op_def [constructor, in funcsem]
goto [constructor, in syntax]
goto1 [constructor, in semantic]
goto1_monotone_for_gammaHeap [constructor, in semantic]
goto_rule [constructor, in semantic]
H
H [definition, in all]
Heap [module, in AlgebraType]
Heap [definition, in semantic]
HeapAlgebraImplem_fs [library]
HeapConnect [definition, in HeapAlgebraImplem_fs]
height_inf [inductive, in ArrayLattice]
height_inf_modify [lemma, in ArrayLattice]
height_inf_modify_set [lemma, in FiniteSetLattice]
hSt [definition, in semantic]
I
If [constructor, in syntax]
ifix_implies_ifix_iter [lemma, in Lattice]
If1 [constructor, in semantic]
If1_monotone_for_gammaHeap [constructor, in semantic]
If2 [constructor, in semantic]
If2_monotone_for_gammaHeap [constructor, in semantic]
if_not_nul_rule [constructor, in semantic]
if_nul_rule [constructor, in semantic]
inf_leaf [constructor, in ArrayLattice]
inf_log [inductive, in PosInf]
inf_log_dec [lemma, in PosInf]
inf_log_dec [lemma, in TabTree]
inf_log_trans [lemma, in TabTree]
inf_log_trans' [lemma, in TabTree]
inf_log_xH [constructor, in PosInf]
inf_log_xI [constructor, in PosInf]
inf_log_xO [constructor, in PosInf]
inf_node [constructor, in ArrayLattice]
initField [definition, in semantic]
initial_State [inductive, in semantic]
initial_state_valid [lemma, in semantic]
init_State [constructor, in semantic]
injN_op [inductive, in funcsem]
injN_op_def [constructor, in funcsem]
injR_op [inductive, in funcsem]
injR_op_def [constructor, in funcsem]
Instruction [inductive, in syntax]
instructionAt [definition, in syntax]
instr_not_new [inductive, in semantic]
integer [definition, in syntax]
invariant_instructionAt [lemma, in semantic]
in_definedFields [lemma, in syntax]
in_inf_log [lemma, in TabTree]
in_rev [lemma, in Lattice]
in_set [definition, in FiniteSetLattice]
in_set_eq [lemma, in FiniteSetLattice]
in_set_monotone [lemma, in FiniteSetLattice]
in_set_singleton [lemma, in FiniteSetLattice]
in_set_singleton' [lemma, in FiniteSetLattice]
in_singleton [lemma, in FiniteSetLattice]
in_singleton_eq [lemma, in FiniteSetLattice]
in_tr [inductive, in semantic]
in_tr_current [constructor, in semantic]
in_tr_rest [constructor, in semantic]
is_bottom [inductive, in ArrayLattice]
is_bottom2_eq' [lemma, in ArrayLattice]
is_bottom_apply [lemma, in ArrayLattice]
is_bottom_dec [lemma, in ArrayLattice]
is_bottom_eq' [lemma, in ArrayLattice]
is_bottom_leaf [constructor, in ArrayLattice]
is_bottom_node [constructor, in ArrayLattice]
iter [definition, in Lattice]
iter_assoc [lemma, in Lattice]
iter_bottom_is_lfp [lemma, in Lattice]
iter_bottom_is_lifp [lemma, in Lattice]
iter_def [lemma, in Lattice]
iter_fix [definition, in Lattice]
iter_listf [definition, in Lattice]
iter_listf_is_monotone [lemma, in Lattice]
iter_monotone [lemma, in Lattice]
iter_stabilize_implies_lfp [lemma, in Lattice]
iter_stabilize_implies_lifp [lemma, in Lattice]
iter_until_fix_f [definition, in Lattice]
J
joinS [definition, in StackLattice]
joinSum [definition, in SumLattice]
joinS_bound1 [definition, in StackLattice]
joinS_bound2 [definition, in StackLattice]
joinS_least_bound [definition, in StackLattice]
join4 [lemma, in Lattice]
join_bool [definition, in BoolLattice]
join_bottom1 [lemma, in Lattice]
join_bottom2 [lemma, in Lattice]
join_eq1 [lemma, in Lattice]
join_eq2 [lemma, in Lattice]
join_list [definition, in Lattice]
join_list_greater [lemma, in Lattice]
join_list_least_greater [lemma, in Lattice]
join_stack_list [definition, in StackLattice]
join_stack_list_not_bot [lemma, in StackLattice]
join_stack_list_same_length [lemma, in StackLattice]
join_sym [lemma, in Lattice]
join_tree [definition, in ArrayLattice]
join_tree_height_inf [lemma, in ArrayLattice]
L
L [definition, in all]
Lattice [inductive, in Lattice]
Lattice [library]
LatticeAtom [inductive, in LatticeAtom]
LatticeAtom [library]
LatticeAtomFiniteSet [definition, in LatticeAtom]
LatticeBool [definition, in BoolLattice]
LatticeFiniteSet [definition, in FiniteSetLattice]
LatticeFunc [definition, in ArrayLattice]
LatticeFuncType [inductive, in ArrayLattice]
LatticeLibrary [library]
leaf [constructor, in TabTree]
lfp [definition, in Lattice]
lfp_is_lfp [lemma, in Lattice]
lfp_is_lifp [lemma, in Lattice]
lfp_list [definition, in Lattice]
lfp_list_is_lifp [lemma, in Lattice]
lift [inductive, in SumLattice]
list_order [inductive, in Lattice]
list_order_cons [constructor, in Lattice]
list_order_join_list [lemma, in Lattice]
list_order_nil [constructor, in Lattice]
load [constructor, in syntax]
load1 [constructor, in semantic]
load1_monotone_for_gammaHeap [constructor, in semantic]
load_rule [constructor, in semantic]
LocalVar [module, in AlgebraType]
LocalVar [definition, in semantic]
LocalVarAlgebraImplem_struct [library]
LocalVarAlgebra1 [definition, in LocalVarAlgebraImplem_struct]
Location [definition, in semantic]
Location_dec [definition, in semantic]
log_inf_log_positive [lemma, in TabTree]
log_positive [definition, in TabTree]
M
max_inf_log_trans [lemma, in TabTree]
max_log_list [definition, in TabTree]
MethodID [definition, in syntax]
MethodName [definition, in syntax]
MethodName_dec [definition, in syntax]
modifyArray [definition, in ArrayLattice]
modifyFunc [definition, in ArrayLattice]
modify_increase [lemma, in ArrayLattice]
modify_monotone [lemma, in ArrayLattice]
modify_set [definition, in FiniteSetLattice]
modify_set_tree [definition, in TabTree]
modify_tree [definition, in TabTree]
N
N [definition, in all]
new [constructor, in syntax]
newLoc_op [inductive, in funcsem]
newLoc_op_def [constructor, in funcsem]
newObject [axiom, in semantic]
newObject_same [axiom, in semantic]
newObject_specif [axiom, in semantic]
new1 [constructor, in semantic]
new_rule [constructor, in semantic]
nextAddress [definition, in syntax]
nil [definition, in syntax]
nil [definition, in ObjectAlgebraImplem_struct]
nil [definition, in syntax]
node [constructor, in TabTree]
nop [constructor, in syntax]
nop1 [constructor, in semantic]
nop1_monotone_for_gammaHeap [constructor, in semantic]
nop_rule [constructor, in semantic]
no_gammaSum_cons_nil [lemma, in StackAlgebraImplem_struct]
nth_positive [definition, in syntax]
null [constructor, in semantic]
num [constructor, in semantic]
Num [module, in AlgebraType]
NumAlgebraImplem_const [library]
NumAlgebraImplem_top [library]
NumconstAlgebra [definition, in NumAlgebraImplem_const]
numop [constructor, in syntax]
numop1 [constructor, in semantic]
numop1_monotone_for_gammaHeap [constructor, in semantic]
numpop_rule [constructor, in semantic]
NumTopAlgebra [definition, in NumAlgebraImplem_top]
O
O [definition, in TabTree]
O [definition, in all]
Object [module, in AlgebraType]
ObjectAlgebra [definition, in ObjectAlgebraImplem_struct]
ObjectAlgebraImplem_struct [library]
OperandStack [definition, in semantic]
Operator [inductive, in syntax]
OpMult [constructor, in syntax]
OpPlus [constructor, in syntax]
orderGamma [definition, in Gamma]
orderGamma_refl [lemma, in Gamma]
orderS [inductive, in StackLattice]
orderS_antisym [definition, in StackLattice]
orderS_length [lemma, in StackLattice]
orderS_refl [definition, in StackLattice]
orderS_trans [definition, in StackLattice]
order' [inductive, in ArrayLattice]
order'_antisym [lemma, in ArrayLattice]
order'_is_bottom [lemma, in ArrayLattice]
order'_is_bottom2 [lemma, in ArrayLattice]
order'_leaf [constructor, in ArrayLattice]
order'_node_leaf [constructor, in ArrayLattice]
order'_node_node [constructor, in ArrayLattice]
order'_trans [lemma, in ArrayLattice]
order_bot_stack [constructor, in StackLattice]
order_cons [constructor, in StackLattice]
order_eq_order [lemma, in Lattice]
order_funcTree' [inductive, in ArrayLattice]
order_funcTree'_none [constructor, in ArrayLattice]
order_funcTree'_some [constructor, in ArrayLattice]
order_func_def [lemma, in ArrayLattice]
order_nil [constructor, in StackLattice]
order_top_stack [constructor, in StackLattice]
P
pcSt [definition, in semantic]
PfCl [definition, in RefAlgebraImplem_class]
PfPt [definition, in RefAlgebraImplem_point]
pop [constructor, in syntax]
pop1 [constructor, in semantic]
pop1_monotone_for_gammaHeap [constructor, in semantic]
pop_op [inductive, in funcsem]
pop_op_def [constructor, in funcsem]
pop_rule [constructor, in semantic]
Poset [inductive, in Poset]
Poset [library]
posInf [definition, in PosInf]
PosInf [library]
positive_dec [lemma, in PosInf]
positive_dec [lemma, in TabTree]
Post [inductive, in Pow]
Post2 [inductive, in Pow]
Post2' [inductive, in Pow]
Post2'_def [constructor, in Pow]
post2_compose_1 [lemma, in Pow]
Post2_def [constructor, in Pow]
post2_monotone [lemma, in Pow]
Post3 [inductive, in Pow]
Post3' [inductive, in Pow]
Post3'_def [constructor, in Pow]
Post3_def [constructor, in Pow]
post_compose_1 [lemma, in Pow]
post_compose_2 [lemma, in Pow]
Post_def [constructor, in Pow]
post_monotone [lemma, in Pow]
pos1of3 [inductive, in rel]
pos1of3_def [constructor, in rel]
pos2of3 [inductive, in rel]
pos2of3_def [constructor, in rel]
pos3of3 [inductive, in rel]
pos3of3_def [constructor, in rel]
Pow [library]
PowPoset [definition, in Pow]
progCount [definition, in syntax]
Program [inductive, in syntax]
push [constructor, in syntax]
push1 [constructor, in semantic]
push1_monotone_for_gammaHeap [constructor, in semantic]
push_op [inductive, in funcsem]
push_op_def [constructor, in funcsem]
push_rule [constructor, in semantic]
putfield [constructor, in syntax]
putfield1 [constructor, in semantic]
putfield1_monotone_for_gammaHeap [constructor, in semantic]
putfield_rule [constructor, in semantic]
putf_op [inductive, in funcsem]
putf_op_def [constructor, in funcsem]
puto'_op [inductive, in funcsem]
puto'_op_def [constructor, in funcsem]
puto_op [inductive, in funcsem]
puto_op_def [constructor, in funcsem]
R
R [definition, in ArrayLattice]
R [definition, in all]
R [definition, in StackLattice]
Ref [module, in AlgebraType]
ref [constructor, in semantic]
RefAlgebraCl [definition, in RefAlgebraImplem_class]
RefAlgebraImplem_class [library]
RefAlgebraImplem_point [library]
RefAlgebraPt [definition, in RefAlgebraImplem_point]
rel [library]
RelCl [inductive, in RefAlgebraImplem_class]
RelCl_def [constructor, in RefAlgebraImplem_class]
RelCl_refl [lemma, in RefAlgebraImplem_class]
RelCl_same_class [lemma, in RefAlgebraImplem_class]
RelContext [definition, in semantic]
RelPt [definition, in RefAlgebraImplem_point]
rule [inductive, in semantic]
rule2instr [definition, in semantic]
R'_acc [lemma, in ArrayLattice]
R_acc [lemma, in ArrayLattice]
R_to_acc_orderS [lemma, in StackLattice]
S
S [definition, in all]
searchClass [definition, in syntax]
searchClass_eq_word [lemma, in syntax]
searchClass_in_class [lemma, in syntax]
searchClass_in_class_nameClass [lemma, in syntax]
searchClass_rec [definition, in syntax]
searchClass_rec_in_l [lemma, in syntax]
searchClass_rec_in_l_classname [lemma, in syntax]
searchField [definition, in syntax]
searchField_rec [definition, in syntax]
secondState [inductive, in semantic]
secondState_def1 [constructor, in semantic]
secondState_def2 [constructor, in semantic]
semantic [library]
SemCol [definition, in semantic]
SemCol' [inductive, in semantic]
SemCol'_valid1 [lemma, in semantic]
SemCol'_valid1' [lemma, in semantic]
SemCol'_valid1_temp [axiom, in semantic]
SemCol'_valid2 [lemma, in semantic]
SemCol'_valid3 [lemma, in semantic]
SemCol'_valid4 [lemma, in semantic]
SemCol_init [constructor, in semantic]
SemCol_next [constructor, in semantic]
sem_binop [definition, in semantic]
sem_binop_op [inductive, in funcsem]
sem_binop_op_def [constructor, in funcsem]
sem_func_correct [lemma, in funcsem]
singleton [definition, in FiniteSetLattice]
SmallStepSem [inductive, in semantic]
SmallStepSemContext [inductive, in semantic]
SmallStepSemContext_def [constructor, in semantic]
SmallStepSemTrace [inductive, in semantic]
SmallStepSemTrace_def [constructor, in semantic]
SmallStepSemTrace_instructionAt [lemma, in correct]
SmallStepSemTrace_SmallStepSem [lemma, in correct]
SmallStepSem_null [lemma, in semantic]
SmallStepSem_star [inductive, in semantic]
SmallStepSem_star_rec [constructor, in semantic]
SmallStepSem_star_0 [constructor, in semantic]
some_stack [constructor, in StackLattice]
some_sum [constructor, in SumLattice]
split_gammaSum_cons_cons [lemma, in StackAlgebraImplem_struct]
Stack [module, in AlgebraType]
stack [inductive, in StackLattice]
StackAlgebra [definition, in StackAlgebraImplem_struct]
StackAlgebraImplem_struct [library]
StackLattice [definition, in StackLattice]
StackLattice [library]
StackPoset [definition, in StackLattice]
State [inductive, in semantic]
store [constructor, in syntax]
store1 [constructor, in semantic]
store1_monotone_for_gammaHeap [constructor, in semantic]
store_op [inductive, in funcsem]
store_op_def [constructor, in funcsem]
store_rule [constructor, in semantic]
substArray [definition, in ArrayLattice]
substField [definition, in semantic]
substFunc [definition, in ArrayLattice]
substHeap [definition, in semantic]
substLocalVar [definition, in semantic]
subst_increase [lemma, in ArrayLattice]
subst_leaf [definition, in TabTree]
subst_monotone [lemma, in ArrayLattice]
subst_tree [definition, in TabTree]
succ_word [definition, in PosInf]
SumLattice [definition, in SumLattice]
SumLattice [library]
SumPoset [definition, in SumLattice]
sum_eq [inductive, in SumLattice]
sum_eq_bot [constructor, in SumLattice]
sum_eq_left [constructor, in SumLattice]
sum_eq_right [constructor, in SumLattice]
sum_eq_top [constructor, in SumLattice]
sum_order [inductive, in SumLattice]
sum_order_bot [constructor, in SumLattice]
sum_order_left [constructor, in SumLattice]
sum_order_right [constructor, in SumLattice]
sum_order_top [constructor, in SumLattice]
syntax [library]
T
TabTree [library]
top [constructor, in NumAlgebraImplem_const]
top [constructor, in NumAlgebraImplem_top]
topF [definition, in ArrayLattice]
topF_is_top [lemma, in ArrayLattice]
top_op [inductive, in funcsem]
top_op_def [constructor, in funcsem]
top_order [constructor, in NumAlgebraImplem_top]
top_order [constructor, in NumAlgebraImplem_const]
top_stack [constructor, in StackLattice]
top_sum [constructor, in SumLattice]
Trace [inductive, in semantic]
Trace_init [constructor, in semantic]
Trace_next [constructor, in semantic]
tree [inductive, in TabTree]
true_order [constructor, in BoolLattice]
typeOfField [inductive, in syntax]
V
V [definition, in all]
valid_trace [definition, in semantic]
valid_trace1 [definition, in semantic]
valid_trace1' [definition, in semantic]
valid_trace2 [definition, in semantic]
valid_trace3 [definition, in semantic]
valid_trace4 [definition, in semantic]
Value [inductive, in semantic]
Value [module, in AlgebraType]
ValueAlgebraImplem_sum2 [library]
ValueAlgebraSum [definition, in ValueAlgebraImplem_sum2]
Var [definition, in syntax]
Var_dec [definition, in syntax]
vtr [definition, in semantic]
VTR [definition, in semantic]
VTrace [definition, in semantic]
W
Word [definition, in PosInf]
WordSize [definition, in PosInf]
word2pos [definition, in PosInf]
Word_1 [definition, in PosInf]
X
xHposInf [definition, in ArrayLattice]
Axiom Index
N
newObject [in semantic]
newObject_same [in semantic]
newObject_specif [in semantic]
S
SemCol'_valid1_temp [in semantic]
Lemma Index
A
AbDef_correct [in ObjectAlgebraImplem_struct]
AbDef_rec_correct [in ObjectAlgebraImplem_struct]
AbInit_correct [in correct]
AbstractSemantic_correct [in correct]
AbTransfMem_correct_aux [in correct]
AbTransfPC_correct [in correct]
AbTransf_correct [in correct]
applyArray_eq_word [in ArrayLattice]
applyArray_monotone [in ArrayLattice]
applyFunc_monotone [in ArrayLattice]
apply_bottom [in ArrayLattice]
apply_build_const_TabTree_is_bot [in TabTree]
apply_build_const_TabTree_is_const [in TabTree]
apply_const [in ArrayLattice]
apply_is_bottom [in ArrayLattice]
apply_join_tree [in ArrayLattice]
apply_modifyArray1 [in ArrayLattice]
apply_modifyArray2 [in ArrayLattice]
apply_modify1 [in ArrayLattice]
apply_modify2 [in ArrayLattice]
apply_modify_eq1 [in ArrayLattice]
apply_modify_eq2 [in ArrayLattice]
apply_modify_set1 [in FiniteSetLattice]
apply_modify_set2 [in FiniteSetLattice]
apply_modify_set_tree [in TabTree]
apply_modify_set_tree1 [in TabTree]
apply_modify_tree1 [in TabTree]
apply_modify_tree2 [in TabTree]
apply_monotone [in ArrayLattice]
apply_set_in [in FiniteSetLattice]
apply_set_tree1 [in TabTree]
apply_substArray1 [in ArrayLattice]
apply_substArray2 [in ArrayLattice]
apply_subst1 [in ArrayLattice]
apply_subst2 [in ArrayLattice]
apply_subst_eq1 [in ArrayLattice]
apply_subst_eq2 [in ArrayLattice]
apply_subst_leaf1 [in TabTree]
apply_subst_leaf2 [in TabTree]
apply_subst_tree1 [in TabTree]
apply_subst_tree2 [in TabTree]
apply_tree_bot [in ArrayLattice]
B
betaTypeOfField_correct [in ObjectAlgebraImplem_struct]
C
class_substField [in semantic]
criterium1 [in Pow]
criterium2 [in Pow]
D
definedFields_eq_word [in syntax]
E
eq'_dec [in ArrayLattice]
eq'_sym [in ArrayLattice]
eq'_to_Feq [in ArrayLattice]
eq'_trans [in ArrayLattice]
eq_order_order [in Lattice]
eq_word_dec [in PosInf]
eq_word_refl [in PosInf]
eq_word_sym [in PosInf]
eq_word_trans [in PosInf]
F
fieldValue_substField1 [in semantic]
fieldValue_substField2 [in semantic]
fix_implies_fix_iter [in Lattice]
Forder_to_order' [in ArrayLattice]
f_in_listf_prop1 [in Lattice]
f_in_listf_prop2 [in Lattice]
f_in_listf_prop3 [in Lattice]
G
gammaHeap_monotone [in correct]
gammaHeap_monotone' [in correct]
gammaLocalVar_monotone [in correct]
gammaMem_monotone [in correct]
GammaMonotone_incl [in Gamma]
gammaStack_monotone [in correct]
H
height_inf_modify [in ArrayLattice]
height_inf_modify_set [in FiniteSetLattice]
I
ifix_implies_ifix_iter [in Lattice]
inf_log_dec [in PosInf]
inf_log_dec [in TabTree]
inf_log_trans [in TabTree]
inf_log_trans' [in TabTree]
initial_state_valid [in semantic]
invariant_instructionAt [in semantic]
in_definedFields [in syntax]
in_inf_log [in TabTree]
in_rev [in Lattice]
in_set_eq [in FiniteSetLattice]
in_set_monotone [in FiniteSetLattice]
in_set_singleton [in FiniteSetLattice]
in_set_singleton' [in FiniteSetLattice]
in_singleton [in FiniteSetLattice]
in_singleton_eq [in FiniteSetLattice]
is_bottom2_eq' [in ArrayLattice]
is_bottom_apply [in ArrayLattice]
is_bottom_dec [in ArrayLattice]
is_bottom_eq' [in ArrayLattice]
iter_assoc [in Lattice]
iter_bottom_is_lfp [in Lattice]
iter_bottom_is_lifp [in Lattice]
iter_def [in Lattice]
iter_listf_is_monotone [in Lattice]
iter_monotone [in Lattice]
iter_stabilize_implies_lfp [in Lattice]
iter_stabilize_implies_lifp [in Lattice]
J
join4 [in Lattice]
join_bottom1 [in Lattice]
join_bottom2 [in Lattice]
join_eq1 [in Lattice]
join_eq2 [in Lattice]
join_list_greater [in Lattice]
join_list_least_greater [in Lattice]
join_stack_list_not_bot [in StackLattice]
join_stack_list_same_length [in StackLattice]
join_sym [in Lattice]
join_tree_height_inf [in ArrayLattice]
L
lfp_is_lfp [in Lattice]
lfp_is_lifp [in Lattice]
lfp_list_is_lifp [in Lattice]
list_order_join_list [in Lattice]
log_inf_log_positive [in TabTree]
M
max_inf_log_trans [in TabTree]
modify_increase [in ArrayLattice]
modify_monotone [in ArrayLattice]
N
no_gammaSum_cons_nil [in StackAlgebraImplem_struct]
O
orderGamma_refl [in Gamma]
orderS_length [in StackLattice]
order'_antisym [in ArrayLattice]
order'_is_bottom [in ArrayLattice]
order'_is_bottom2 [in ArrayLattice]
order'_trans [in ArrayLattice]
order_eq_order [in Lattice]
order_func_def [in ArrayLattice]
P
positive_dec [in PosInf]
positive_dec [in TabTree]
post2_compose_1 [in Pow]
post2_monotone [in Pow]
post_compose_1 [in Pow]
post_compose_2 [in Pow]
post_monotone [in Pow]
R
RelCl_refl [in RefAlgebraImplem_class]
RelCl_same_class [in RefAlgebraImplem_class]
R'_acc [in ArrayLattice]
R_acc [in ArrayLattice]
R_to_acc_orderS [in StackLattice]
S
searchClass_eq_word [in syntax]
searchClass_in_class [in syntax]
searchClass_in_class_nameClass [in syntax]
searchClass_rec_in_l [in syntax]
searchClass_rec_in_l_classname [in syntax]
SemCol'_valid1 [in semantic]
SemCol'_valid1' [in semantic]
SemCol'_valid2 [in semantic]
SemCol'_valid3 [in semantic]
SemCol'_valid4 [in semantic]
sem_func_correct [in funcsem]
SmallStepSemTrace_instructionAt [in correct]
SmallStepSemTrace_SmallStepSem [in correct]
SmallStepSem_null [in semantic]
split_gammaSum_cons_cons [in StackAlgebraImplem_struct]
subst_increase [in ArrayLattice]
subst_monotone [in ArrayLattice]
T
topF_is_top [in ArrayLattice]
Constructor Index
A
AbMemOrder_def [in correct]
B
bot [in NumAlgebraImplem_const]
bot_order [in NumAlgebraImplem_const]
bot_stack [in StackLattice]
bot_sum [in SumLattice]
C
compose1_def [in rel]
compose2_def [in Pow]
compose2_def [in rel]
compose3_def [in rel]
compose_def [in Pow]
config [in semantic]
const [in NumAlgebraImplem_const]
const_def [in rel]
const_order [in NumAlgebraImplem_const]
D
def_op_def [in funcsem]
E
eq'_leaf [in ArrayLattice]
eq'_leaf_node [in ArrayLattice]
eq'_node_leaf [in ArrayLattice]
eq'_node_node [in ArrayLattice]
eq_bot_stack [in StackLattice]
eq_cons [in StackLattice]
eq_funcTree'_none [in ArrayLattice]
eq_funcTree'_some [in ArrayLattice]
eq_nil [in StackLattice]
eq_top_stack [in StackLattice]
F
false_order [in BoolLattice]
fieldNum [in syntax]
fieldRef [in syntax]
frame [in semantic]
G
gammaMem_def [in correct]
gammaSt_def [in correct]
gammaSum_cons [in StackAlgebraImplem_struct]
gammaSum_nil [in StackAlgebraImplem_struct]
getfield [in syntax]
getfield1 [in semantic]
getfield1_monotone_for_gammaHeap [in semantic]
getfield_rule [in semantic]
getf_op_def [in funcsem]
getN_op_def [in funcsem]
geto_op_def [in funcsem]
getR_op_def [in funcsem]
get_op_def [in funcsem]
goto [in syntax]
goto1 [in semantic]
goto1_monotone_for_gammaHeap [in semantic]
goto_rule [in semantic]
I
If [in syntax]
If1 [in semantic]
If1_monotone_for_gammaHeap [in semantic]
If2 [in semantic]
If2_monotone_for_gammaHeap [in semantic]
if_not_nul_rule [in semantic]
if_nul_rule [in semantic]
inf_leaf [in ArrayLattice]
inf_log_xH [in PosInf]
inf_log_xI [in PosInf]
inf_log_xO [in PosInf]
inf_node [in ArrayLattice]
init_State [in semantic]
injN_op_def [in funcsem]
injR_op_def [in funcsem]
in_tr_current [in semantic]
in_tr_rest [in semantic]
is_bottom_leaf [in ArrayLattice]
is_bottom_node [in ArrayLattice]
L
leaf [in TabTree]
list_order_cons [in Lattice]
list_order_nil [in Lattice]
load [in syntax]
load1 [in semantic]
load1_monotone_for_gammaHeap [in semantic]
load_rule [in semantic]
N
new [in syntax]
newLoc_op_def [in funcsem]
new1 [in semantic]
new_rule [in semantic]
node [in TabTree]
nop [in syntax]
nop1 [in semantic]
nop1_monotone_for_gammaHeap [in semantic]
nop_rule [in semantic]
null [in semantic]
num [in semantic]
numop [in syntax]
numop1 [in semantic]
numop1_monotone_for_gammaHeap [in semantic]
numpop_rule [in semantic]
O
OpMult [in syntax]
OpPlus [in syntax]
order'_leaf [in ArrayLattice]
order'_node_leaf [in ArrayLattice]
order'_node_node [in ArrayLattice]
order_bot_stack [in StackLattice]
order_cons [in StackLattice]
order_funcTree'_none [in ArrayLattice]
order_funcTree'_some [in ArrayLattice]
order_nil [in StackLattice]
order_top_stack [in StackLattice]
P
pop [in syntax]
pop1 [in semantic]
pop1_monotone_for_gammaHeap [in semantic]
pop_op_def [in funcsem]
pop_rule [in semantic]
Post2'_def [in Pow]
Post2_def [in Pow]
Post3'_def [in Pow]
Post3_def [in Pow]
Post_def [in Pow]
pos1of3_def [in rel]
pos2of3_def [in rel]
pos3of3_def [in rel]
push [in syntax]
push1 [in semantic]
push1_monotone_for_gammaHeap [in semantic]
push_op_def [in funcsem]
push_rule [in semantic]
putfield [in syntax]
putfield1 [in semantic]
putfield1_monotone_for_gammaHeap [in semantic]
putfield_rule [in semantic]
putf_op_def [in funcsem]
puto'_op_def [in funcsem]
puto_op_def [in funcsem]
R
ref [in semantic]
RelCl_def [in RefAlgebraImplem_class]
S
secondState_def1 [in semantic]
secondState_def2 [in semantic]
SemCol_init [in semantic]
SemCol_next [in semantic]
sem_binop_op_def [in funcsem]
SmallStepSemContext_def [in semantic]
SmallStepSemTrace_def [in semantic]
SmallStepSem_star_rec [in semantic]
SmallStepSem_star_0 [in semantic]
some_stack [in StackLattice]
some_sum [in SumLattice]
store [in syntax]
store1 [in semantic]
store1_monotone_for_gammaHeap [in semantic]
store_op_def [in funcsem]
store_rule [in semantic]
sum_eq_bot [in SumLattice]
sum_eq_left [in SumLattice]
sum_eq_right [in SumLattice]
sum_eq_top [in SumLattice]
sum_order_bot [in SumLattice]
sum_order_left [in SumLattice]
sum_order_right [in SumLattice]
sum_order_top [in SumLattice]
T
top [in NumAlgebraImplem_const]
top [in NumAlgebraImplem_top]
top_op_def [in funcsem]
top_order [in NumAlgebraImplem_top]
top_order [in NumAlgebraImplem_const]
top_stack [in StackLattice]
top_sum [in SumLattice]
Trace_init [in semantic]
Trace_next [in semantic]
true_order [in BoolLattice]
Inductive Index
A
AbMem [in correct]
AbMemOrder [in correct]
AbNumConst [in NumAlgebraImplem_const]
AbNumConstOrder [in NumAlgebraImplem_const]
AbNumTop [in NumAlgebraImplem_top]
AbNumTopOrder [in NumAlgebraImplem_top]
B
bool_order [in BoolLattice]
C
Class [in syntax]
ClassInst [in semantic]
compose [in Pow]
compose1 [in rel]
compose2 [in Pow]
compose2 [in rel]
compose3 [in rel]
Connect [in AlgebraType]
Connect [in AlgebraType]
Connect [in AlgebraType]
Connect [in AlgebraType]
Connect [in AlgebraType]
Connect [in AlgebraType]
Connect [in AlgebraType]
const [in rel]
D
def_op [in funcsem]
E
eqS [in StackLattice]
eq' [in ArrayLattice]
eq_funcTree' [in ArrayLattice]
F
Field [in syntax]
Frame [in semantic]
FuncSem [in funcsem]
funcTree [in ArrayLattice]
G
Gamma [in Gamma]
GammaBestTop [in Gamma]
gammaMem [in correct]
gammaSt [in correct]
gammaSum [in StackAlgebraImplem_struct]
GammaTop [in Gamma]
getf_op [in funcsem]
getN_op [in funcsem]
geto_op [in funcsem]
getR_op [in funcsem]
get_op [in funcsem]
H
height_inf [in ArrayLattice]
I
inf_log [in PosInf]
initial_State [in semantic]
injN_op [in funcsem]
injR_op [in funcsem]
Instruction [in syntax]
instr_not_new [in semantic]
in_tr [in semantic]
is_bottom [in ArrayLattice]
L
Lattice [in Lattice]
LatticeAtom [in LatticeAtom]
LatticeFuncType [in ArrayLattice]
lift [in SumLattice]
list_order [in Lattice]
N
newLoc_op [in funcsem]
O
Operator [in syntax]
orderS [in StackLattice]
order' [in ArrayLattice]
order_funcTree' [in ArrayLattice]
P
pop_op [in funcsem]
Poset [in Poset]
Post [in Pow]
Post2 [in Pow]
Post2' [in Pow]
Post3 [in Pow]
Post3' [in Pow]
pos1of3 [in rel]
pos2of3 [in rel]
pos3of3 [in rel]
Program [in syntax]
push_op [in funcsem]
putf_op [in funcsem]
puto'_op [in funcsem]
puto_op [in funcsem]
R
RelCl [in RefAlgebraImplem_class]
rule [in semantic]
S
secondState [in semantic]
SemCol' [in semantic]
sem_binop_op [in funcsem]
SmallStepSem [in semantic]
SmallStepSemContext [in semantic]
SmallStepSemTrace [in semantic]
SmallStepSem_star [in semantic]
stack [in StackLattice]
State [in semantic]
store_op [in funcsem]
sum_eq [in SumLattice]
sum_order [in SumLattice]
T
top_op [in funcsem]
Trace [in semantic]
tree [in TabTree]
typeOfField [in syntax]
V
Value [in semantic]
Definition Index
A
AbDef [in ObjectAlgebraImplem_struct]
AbDef_rec [in ObjectAlgebraImplem_struct]
AbInit [in correct]
AbNumConstjoin [in NumAlgebraImplem_const]
AbNumConstLattice [in NumAlgebraImplem_const]
AbNumConstPoset [in NumAlgebraImplem_const]
AbNumTopjoin [in NumAlgebraImplem_top]
AbNumTopLattice [in NumAlgebraImplem_top]
AbNumTopPoset [in NumAlgebraImplem_top]
AbState [in correct]
AbstractSemantic [in correct]
AbTransfMem [in correct]
AbTransPC [in correct]
accR_property_some_stack [in StackLattice]
accS_property [in StackLattice]
acc_property_bot [in StackLattice]
acc_property_const [in NumAlgebraImplem_const]
acc_property_some_stack [in StackLattice]
acc_property_top [in StackLattice]
acc_property_top [in NumAlgebraImplem_const]
applyArray [in ArrayLattice]
applyFunc [in ArrayLattice]
apply_functree [in ArrayLattice]
apply_set [in FiniteSetLattice]
apply_set_tree [in TabTree]
apply_tree [in TabTree]
ArrayLattice [in ArrayLattice]
ArrayPoset [in ArrayLattice]
B
betaTypeOfField [in ObjectAlgebraImplem_struct]
BoolPoset [in BoolLattice]
build_const_TabTree_rec [in TabTree]
C
CallStack [in semantic]
ClassName [in syntax]
const [in ArrayLattice]
Context [in semantic]
correct1 [in Pow]
correct2 [in Pow]
Ct [in semantic]
currentState [in semantic]
D
def [in semantic]
definedFields [in syntax]
E
eqS_dec [in StackLattice]
eqS_refl [in StackLattice]
eqS_sym [in StackLattice]
eqS_trans [in StackLattice]
eq_dec [in Lattice]
eq_word [in PosInf]
F
Fbottom [in ArrayLattice]
Fcompose [in Pow]
Fcompose2 [in Pow]
Feq [in ArrayLattice]
FieldName [in syntax]
Field_dec [in syntax]
FiniteSet [in FiniteSetLattice]
Fjoin [in ArrayLattice]
funcTree' [in ArrayLattice]
funcTree_Lattice [in ArrayLattice]
funcTree_Poset [in ArrayLattice]
G
gammaBestTopRefPt [in RefAlgebraImplem_point]
gammaCl [in RefAlgebraImplem_class]
gammaHeap [in HeapAlgebraImplem_fs]
gammaLocalVar1 [in LocalVarAlgebraImplem_struct]
GammaMonotone [in Gamma]
gammaNumConst [in NumAlgebraImplem_const]
gammaNumTop [in NumAlgebraImplem_top]
gammaObjectPointWise [in ObjectAlgebraImplem_struct]
gammaPt [in RefAlgebraImplem_point]
gammaRefCl [in RefAlgebraImplem_class]
gammaRefPt [in RefAlgebraImplem_point]
gammaStack [in StackAlgebraImplem_struct]
gammaTopBestRefCl [in RefAlgebraImplem_class]
gammaTopNumConst [in NumAlgebraImplem_const]
gammaTopNumTop [in NumAlgebraImplem_top]
gammaTopObjectPointWise [in ObjectAlgebraImplem_struct]
gammaTopRefCl [in RefAlgebraImplem_class]
gammaTopRefPt [in RefAlgebraImplem_point]
gammaTopValueSum [in ValueAlgebraImplem_sum2]
gammaValueSum [in ValueAlgebraImplem_sum2]
H
H [in all]
Heap [in semantic]
HeapConnect [in HeapAlgebraImplem_fs]
hSt [in semantic]
I
initField [in semantic]
instructionAt [in syntax]
integer [in syntax]
in_set [in FiniteSetLattice]
iter [in Lattice]
iter_fix [in Lattice]
iter_listf [in Lattice]
iter_until_fix_f [in Lattice]
J
joinS [in StackLattice]
joinSum [in SumLattice]
joinS_bound1 [in StackLattice]
joinS_bound2 [in StackLattice]
joinS_least_bound [in StackLattice]
join_bool [in BoolLattice]
join_list [in Lattice]
join_stack_list [in StackLattice]
join_tree [in ArrayLattice]
L
L [in all]
LatticeAtomFiniteSet [in LatticeAtom]
LatticeBool [in BoolLattice]
LatticeFiniteSet [in FiniteSetLattice]
LatticeFunc [in ArrayLattice]
lfp [in Lattice]
lfp_list [in Lattice]
LocalVar [in semantic]
LocalVarAlgebra1 [in LocalVarAlgebraImplem_struct]
Location [in semantic]
Location_dec [in semantic]
log_positive [in TabTree]
M
max_log_list [in TabTree]
MethodID [in syntax]
MethodName [in syntax]
MethodName_dec [in syntax]
modifyArray [in ArrayLattice]
modifyFunc [in ArrayLattice]
modify_set [in FiniteSetLattice]
modify_set_tree [in TabTree]
modify_tree [in TabTree]
N
N [in all]
nextAddress [in syntax]
nil [in syntax]
nil [in ObjectAlgebraImplem_struct]
nil [in syntax]
nth_positive [in syntax]
NumconstAlgebra [in NumAlgebraImplem_const]
NumTopAlgebra [in NumAlgebraImplem_top]
O
O [in TabTree]
O [in all]
ObjectAlgebra [in ObjectAlgebraImplem_struct]
OperandStack [in semantic]
orderGamma [in Gamma]
orderS_antisym [in StackLattice]
orderS_refl [in StackLattice]
orderS_trans [in StackLattice]
P
pcSt [in semantic]
PfCl [in RefAlgebraImplem_class]
PfPt [in RefAlgebraImplem_point]
posInf [in PosInf]
PowPoset [in Pow]
progCount [in syntax]
R
R [in ArrayLattice]
R [in all]
R [in StackLattice]
RefAlgebraCl [in RefAlgebraImplem_class]
RefAlgebraPt [in RefAlgebraImplem_point]
RelContext [in semantic]
RelPt [in RefAlgebraImplem_point]
rule2instr [in semantic]
S
S [in all]
searchClass [in syntax]
searchClass_rec [in syntax]
searchField [in syntax]
searchField_rec [in syntax]
SemCol [in semantic]
sem_binop [in semantic]
singleton [in FiniteSetLattice]
StackAlgebra [in StackAlgebraImplem_struct]
StackLattice [in StackLattice]
StackPoset [in StackLattice]
substArray [in ArrayLattice]
substField [in semantic]
substFunc [in ArrayLattice]
substHeap [in semantic]
substLocalVar [in semantic]
subst_leaf [in TabTree]
subst_tree [in TabTree]
succ_word [in PosInf]
SumLattice [in SumLattice]
SumPoset [in SumLattice]
T
topF [in ArrayLattice]
V
V [in all]
valid_trace [in semantic]
valid_trace1 [in semantic]
valid_trace1' [in semantic]
valid_trace2 [in semantic]
valid_trace3 [in semantic]
valid_trace4 [in semantic]
ValueAlgebraSum [in ValueAlgebraImplem_sum2]
Var [in syntax]
Var_dec [in syntax]
vtr [in semantic]
VTR [in semantic]
VTrace [in semantic]
W
Word [in PosInf]
WordSize [in PosInf]
word2pos [in PosInf]
Word_1 [in PosInf]
X
xHposInf [in ArrayLattice]
Module Index
H
Heap [in AlgebraType]
L
LocalVar [in AlgebraType]
N
Num [in AlgebraType]
O
Object [in AlgebraType]
R
Ref [in AlgebraType]
S
Stack [in AlgebraType]
V
Value [in AlgebraType]
Library Index
A
AlgebraType
all
ArrayLattice
B
BoolLattice
C
correct
F
FiniteSetLattice
funcsem
G
Gamma
H
HeapAlgebraImplem_fs
L
Lattice
LatticeAtom
LatticeLibrary
LocalVarAlgebraImplem_struct
N
NumAlgebraImplem_const
NumAlgebraImplem_top
O
ObjectAlgebraImplem_struct
P
Poset
PosInf
Pow
R
RefAlgebraImplem_class
RefAlgebraImplem_point
rel
S
semantic
StackAlgebraImplem_struct
StackLattice
SumLattice
syntax
T
TabTree
V
ValueAlgebraImplem_sum2
| 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 |
_ |
(640 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 |
_ |
(4 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 |
_ |
(157 entries) |
| Constructor 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 |
_ |
(159 entries) |
| Inductive 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 |
_ |
(94 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 |
_ |
(190 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 |
_ |
(7 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 |
_ |
(29 entries) |
This page has been generated by coqdoc