\generic G;defined in: instanceAllocation.key Line: 6 Offset :4\generic H \extends Object ;defined in: instanceAllocation.key Line: 7 Offset :4\generic J \extends Object ;defined in: instanceAllocation.key Line: 8 Offset :4\generic K;defined in: instanceAllocation.key Line: 9 Offset :4\generic alphaObj \extends Object ;defined in: instanceAllocation.key Line: 10 Offset :4\generic betaObj \extends Object ;defined in: instanceAllocation.key Line: 11 Offset :4instanceCreationUnfoldArguments {
\find ( \modality{#allmodal}{.. #nsn ...}\endmodality ( post ))
\replacewith ( \modality{#allmodal}{.. #evaluate-arguments(#nsn); ...}\endmodality ( post ))
\heuristics (simplify_autoname )
};defined in: instanceAllocation.key Line: 62 Offset :4instanceCreationAssignmentUnfoldArguments {
\find ( \modality{#allmodal}{.. #lhs = #nsn; ...}\endmodality ( post ))
\replacewith ( \modality{#allmodal}{.. #evaluate-arguments(#lhs = #nsn); ...}\endmodality ( post ))
\heuristics (simplify_autoname )
};defined in: instanceAllocation.key Line: 68 Offset :4instanceCreation {
\find ( \modality{#allmodal}{.. #n ...}\endmodality ( post ))
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#v0) #v0 = #create-object(#n);
#constructor-call(#v0, #n);
#post-work(#v0); ...}\endmodality ( post ))
\heuristics (method_expand )
};defined in: instanceAllocation.key Line: 74 Offset :4instanceCreationAssignment {
\schemaVar \modalOperator { diamond , box } #normal;
\find ( \modality{#normal}{.. #lhs = #n; ...}\endmodality ( post ))
\varcond \replacewith ( \modality{#normal}{.. #typeof(#v0) #v0 = #create-object(#n);
#constructor-call(#v0, #n);
#post-work(#v0);
#lhs = #v0;
...}\endmodality ( post ))
\heuristics (method_expand )
};defined in: instanceAllocation.key Line: 83 Offset :4allocateInstance {
\find ( ==> \modality{#allmodal}{.#pm@#t2().. #lhs = #t.#allocate()@#t; ...}\endmodality ( post ))
\varcond \replacewith ( ==> { heap := create ( heap , #lhs)|| permissions := create ( permissions , #lhs)} \modality{#allmodal}{.. ...}\endmodality ( post )) \add ( #lhs!= null & ( wellFormed ( heap )-> boolean :: select ( heap , #lhs, java.lang.Object :: )= FALSE )& ( wellFormed ( permissions )-> boolean :: select ( permissions , #lhs, java.lang.Object :: )= FALSE )& alphaObj :: exactInstance ( #lhs)= TRUE ==> )
\heuristics (method_expand )
};defined in: instanceAllocation.key Line: 98 Offset :4allocateInstanceWithLength {
\find ( ==> \modality{#allmodal}{.#pm@#t2().. #lhs = #t.#allocate(#len)@#t; ...}\endmodality ( post ))
\varcond \replacewith ( ==> { heap := store ( store ( create ( heap , #lhs), #lhs, java.lang.Object :: , 0 ), #lhs, java.lang.Object :: , FALSE )|| permissions := create ( permissions , #lhs)} \modality{#allmodal}{.. ...}\endmodality ( post )) \add ( #lhs!= null & ( wellFormed ( heap )-> ( boolean :: select ( heap , #lhs, java.lang.Object :: )= FALSE & length ( #lhs)= #len))& ( wellFormed ( permissions )-> boolean :: select ( permissions , #lhs, java.lang.Object :: )= FALSE )& alphaObj :: exactInstance ( #lhs)= TRUE ==> )
\heuristics (method_expand )
};defined in: instanceAllocation.key Line: 115 Offset :4allocateInstance {
\find ( ==> \modality{#allmodal}{.#pm@#t2().. #lhs = #t.#allocate()@#t; ...}\endmodality ( post ))
\varcond \replacewith ( ==> { heap := create ( heap , #lhs)} \modality{#allmodal}{.. ...}\endmodality ( post )) \add ( #lhs!= null & ( wellFormed ( heap )-> boolean :: select ( heap , #lhs, java.lang.Object :: )= FALSE )& alphaObj :: exactInstance ( #lhs)= TRUE ==> )
\heuristics (method_expand )
};defined in: instanceAllocation.key Line: 138 Offset :4allocateInstanceWithLength {
\find ( ==> \modality{#allmodal}{.#pm@#t2().. #lhs = #t.#allocate(#len)@#t; ...}\endmodality ( post ))
\varcond \replacewith ( ==> { heap := store ( store ( create ( heap , #lhs), #lhs, java.lang.Object :: , 0 ), #lhs, java.lang.Object :: , FALSE )} \modality{#allmodal}{.. ...}\endmodality ( post )) \add ( #lhs!= null & ( wellFormed ( heap )-> ( boolean :: select ( heap , #lhs, java.lang.Object :: )= FALSE & length ( #lhs)= #len))& alphaObj :: exactInstance ( #lhs)= TRUE ==> )
\heuristics (method_expand )
};defined in: instanceAllocation.key Line: 150 Offset :4special_constructor_call {
\find ( \modality{#allmodal}{.. #scr ...}\endmodality ( post ))
\replacewith ( \modality{#allmodal}{.. #special-constructor-call(#scr); ...}\endmodality ( post ))
\heuristics (method_expand )
};defined in: instanceAllocation.key Line: 171 Offset :4arrayCreation {
\schemaVar \modalOperator { diamond , box } #normal;
\find ( \modality{#normal}{.. #lhs = #na; ...}\endmodality ( post ))
\varcond \replacewith ( \modality{#normal}{..
#typeof(#na) #v0;
#init-array-creation(#v0, #na);
#lhs = #v0; ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: instanceAllocation.key Line: 182 Offset :4arrayCreationWithInitializers {
\find ( \modality{#allmodal}{.. #lhs = #arrayinitializer; ...}\endmodality ( post ))
\varcond \replacewith ( \modality{#allmodal}{..
#typeof(#lhs) #v0;
#init-array-creation(#v0, #arrayinitializer);
#lhs = #v0; ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: instanceAllocation.key Line: 193 Offset :4exact_instance_definition_int {
\find ( int :: exactInstance ( idx0 )= TRUE )
\varcond \replacewith ( \exists iv ; ( idx0 = iv ))
\heuristics (simplify )
};defined in: instanceAllocation.key Line: 213 Offset :4exact_instance_definition_boolean {
\find ( boolean :: exactInstance ( bool )= TRUE )
\varcond \replacewith ( \exists bv ; ( bool = bv ))
\heuristics (simplify )
};defined in: instanceAllocation.key Line: 220 Offset :4exact_instance_definition_null {
\find ( Null :: exactInstance ( obj )= TRUE )
\varcond \replacewith ( obj = null )
\heuristics (simplify )
};defined in: instanceAllocation.key Line: 227 Offset :4exact_instance_for_interfaces_or_abstract_classes {
\find ( G :: exactInstance ( obj ))
\varcond \replacewith ( FALSE )
\heuristics (simplify )
\displayname "interfaces or abstract classes have no exact instances"
};defined in: instanceAllocation.key Line: 234 Offset :4