poolKeyIsContentOfValue {
\schemaVar \term Seq slit ;
\find ( strContent ( strPool ( slit )))
\replacewith ( slit )
\heuristics (simplify )
};defined in: String.key Line: 6 Offset :2poolIsInjective {
\schemaVar \term Seq slit1 , slit2 ;
\find ( strPool ( slit1 )= strPool ( slit2 ))
\replacewith ( slit1 = slit2 )
\heuristics (simplify )
};defined in: String.key Line: 14 Offset :2insert_constant_string_value {
\schemaVar \program ConstantStringVariable #csv;
\assumes ( wellFormed ( heap )==> )
\find ( #csv)
\sameUpdateLevel
\replacewith ( \if ( #constantvalue ( #csv)= null )\then ( null )\else ( strPool ( (Seq ) #constantvalue ( #csv)))) \add ( #constantvalue ( #csv)= null | ( strPool ( (Seq ) #constantvalue ( #csv))!= null & select <[ boolean ]> ( heap , strPool ( (Seq ) #constantvalue ( #csv)), java.lang.Object :: #$created)= TRUE )==> )
\heuristics (concrete )
};defined in: String.key Line: 22 Offset :2nullString {
\find ( strContent ( null ))
\replacewith ( "null" )
\heuristics (concrete )
};defined in: String.key Line: 35 Offset :2stringAssignment {
\schemaVar \modalOperator { diamond , box } #normalassign;
\schemaVar \program Variable #v;
\schemaVar \program StringLiteral #slit;
\schemaVar \formula post ;
\find ( \modality{#normalassign}{.. #v = #slit; ...}\endmodality ( post ))
\sameUpdateLevel
\replacewith ( { #v:= strPool ( #slit)} \modality{#normalassign}{.. ...}\endmodality ( post )) \add ( strPool ( #slit)!= null , select <[ boolean ]> ( heap , strPool ( #slit), java.lang.Object :: #$created)= TRUE ==> )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 45 Offset :2stringConcat {
\schemaVar \modalOperator { diamond , box } #normalassign;
\schemaVar \program Variable #v;
\schemaVar \program SimpleStringExpression #sstr1, #sstr2;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign} {..
#v = #sstr1 + #sstr2;
...}\endmodality ( post ))
\sameUpdateLevel
\varcond \replacewith ( { #v:= sk } { heap := create ( heap , sk )} \modality{#normalassign}{.. ...}\endmodality ( post )) \add ( strContent ( sk )= seqConcat ( strContent ( #sstr1), strContent ( #sstr2))==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 65 Offset :2stringConcatIntExpLeft {
\schemaVar \modalOperator { diamond , box } #normalassign;
\schemaVar \program Variable #v;
\schemaVar \program SimpleStringExpression #sstrRight;
\schemaVar \program AnyJavaTypeExpression #seLeft;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign}
{.. #v = #seLeft + #sstrRight; ...}
\endmodality ( post ))
\sameUpdateLevel
\varcond \replacewith ( { #v:= sk } { heap := create ( heap , sk )} \modality{#normalassign}{.. ...}\endmodality ( post )) \add ( strContent ( sk )= seqConcat ( clTranslateInt ( #seLeft), strContent ( #sstrRight))==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 86 Offset :2stringConcatIntExpRight {
\schemaVar \modalOperator { diamond , box } #normalassign;
\schemaVar \program Variable #v;
\schemaVar \program SimpleStringExpression #sstrLeft;
\schemaVar \program AnyJavaTypeExpression #seRight;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign}
{.. #v = #sstrLeft + #seRight; ...}
\endmodality ( post ))
\sameUpdateLevel
\varcond \replacewith ( { #v:= sk } { heap := create ( heap , sk )} \modality{#normalassign}{.. ...}\endmodality ( post )) \add ( strContent ( sk )= seqConcat ( strContent ( #sstrLeft), clTranslateInt ( #seRight))==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 108 Offset :2stringConcatCharExpLeft {
\schemaVar \modalOperator { diamond , box } #normalassign;
\schemaVar \program Variable #v;
\schemaVar \program SimpleStringExpression #sstrRight;
\schemaVar \program JavaCharExpression #seLeft;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign}
{.. #v = #seLeft + #sstrRight; ...}
\endmodality ( post ))
\sameUpdateLevel
\varcond \replacewith ( { #v:= sk } { heap := create ( heap , sk )} \modality{#normalassign}{.. ...}\endmodality ( post )) \add ( strContent ( sk )= seqConcat ( seqSingleton ( #seLeft), strContent ( #sstrRight))==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 129 Offset :2stringConcatCharExpRight {
\schemaVar \modalOperator { diamond , box } #normalassign;
\schemaVar \program Variable #v;
\schemaVar \program SimpleStringExpression #sstrLeft;
\schemaVar \program JavaCharExpression #seRight;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign}
{.. #v = #sstrLeft + #seRight; ...}
\endmodality ( post ))
\sameUpdateLevel
\varcond \replacewith ( { #v:= sk } { heap := create ( heap , sk )} \modality{#normalassign}{.. ...}\endmodality ( post )) \add ( strContent ( sk )= seqConcat ( strContent ( #sstrLeft), seqSingleton ( #seRight))==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 151 Offset :2stringConcatBooleanLeft {
\schemaVar \modalOperator { diamond , box } #normalassign;
\schemaVar \program Variable #v;
\schemaVar \program SimpleStringExpression #sstrRight;
\schemaVar \program SimpleJavaBooleanExpression #seLeft;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign}
{.. #v = #seLeft + #sstrRight; ...}
\endmodality ( post ))
\sameUpdateLevel
\varcond \replacewith ( { #v:= sk } { heap := create ( heap , sk )} \modality{#normalassign}{.. ...}\endmodality ( post )) \add ( strContent ( sk )= seqConcat ( \if ( #seLeft= TRUE )\then ( "true" )\else ( "false" ), strContent ( #sstrRight))==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 172 Offset :2stringConcatBooleanRight {
\schemaVar \modalOperator { diamond , box } #normalassign;
\schemaVar \program Variable #v;
\schemaVar \program SimpleStringExpression #sstrLeft;
\schemaVar \program SimpleJavaBooleanExpression #seRight;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign}
{.. #v = #sstrLeft + #seRight; ...}
\endmodality ( post ))
\sameUpdateLevel
\varcond \replacewith ( { #v:= sk } { heap := create ( heap , sk )} \modality{#normalassign}{.. ...}\endmodality ( post )) \add ( strContent ( sk )= seqConcat ( strContent ( #sstrLeft), \if ( #seRight= TRUE )\then ( "true" )\else ( "false" ))==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 197 Offset :2stringConcatObjectLeft {
\schemaVar \modalOperator { diamond , box } #normalassign;
\schemaVar \program Variable #v;
\schemaVar \program SimpleStringExpression #sstrRight;
\schemaVar \program SimpleNonStringObjectExpression #seLeft;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign}
{.. #v = #seLeft + #sstrRight; ...}
\endmodality ( post ))
\sameUpdateLevel
\varcond "#seLeft not null" : \replacewith ( \modality{#normalassign}
{.. #v = #seLeft.toString() + #sstrRight; ...}
\endmodality ( post )) \add ( ==> #seLeft= null );
"#seLeft null" : \replacewith ( { #v:= sk } { heap := create ( heap , sk )} \modality{#normalassign}{.. ...}\endmodality ( post )) \add ( #seLeft= null , strContent ( sk )= seqConcat ( strContent ( null ), strContent ( #sstrRight))==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 222 Offset :2stringConcatObjectRight {
\schemaVar \modalOperator { diamond , box } #normalassign;
\schemaVar \program Variable #v;
\schemaVar \program SimpleStringExpression #sstrLeft;
\schemaVar \program SimpleNonStringObjectExpression #seRight;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign}
{.. #v = #sstrLeft + #seRight; ...}
\endmodality ( post ))
\sameUpdateLevel
\varcond "#seRight not null" : \replacewith ( \modality{#normalassign}
{.. #v = #sstrLeft + #seRight.toString(); ...}
\endmodality ( post )) \add ( ==> #seRight= null );
"#seRight null" : \replacewith ( { #v:= sk } { heap := create ( heap , sk )} \modality{#normalassign}{.. ...}\endmodality ( post )) \add ( #seRight= null , strContent ( sk )= seqConcat ( strContent ( #sstrLeft), strContent ( null ))==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 253 Offset :2