evaluateAssertCondition_1 {
\find ( \modality{#allmodal}{.. assert #nse1; ...}\endmodality ( b ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nse1) #condition = #nse1;
assert #condition; ...}\endmodality ( b ) )
\heuristics (simplify_prog )
\displayname "evaluate assert condition"
};defined in: assertions.key Line: 19 Offset :4evaluateAssertCondition_2 {
\find ( \modality{#allmodal}{.. assert #nse1 : #e; ...}\endmodality ( b ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nse1) #condition = #nse1;
assert #condition : #e; ...}\endmodality ( b ) )
\heuristics (simplify_prog )
\displayname "evaluate assert condition"
};defined in: assertions.key Line: 28 Offset :4evaluateAssertMessage {
\find ( \modality{#allmodal}{.. assert #se1 : #nse2; ...}\endmodality ( b ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nse2) #message = #nse2;
assert #se1 : #message; ...}\endmodality ( b ) )
\heuristics (simplify_prog )
\displayname "evaluate assert condition"
};defined in: assertions.key Line: 37 Offset :4assert {
\find ( \modality{#allmodal}{.. assert #se1; ...}\endmodality ( b ) )
"Assertion (#se1) OK" : \replacewith ( \modality{#allmodal}{.. ...}\endmodality ( b ) ) \add ( #se1 = TRUE ==> ) ;
"Assertion (#se1) Failure" : \replacewith ( \modality{#allmodal}{.. throw new java.lang.AssertionError(); ...}\endmodality ( b ) ) \add ( #se1 = FALSE ==> )
\heuristics (simplify_prog )
\displayname "assert"
};defined in: assertions.key Line: 46 Offset :4assertWithReferenceMessage {
\find ( \modality{#allmodal}{.. assert #se1 : #se2; ...}\endmodality ( b ) )
\varcond "Assertion (#se1) OK" : \replacewith ( \modality{#allmodal}{.. ...}\endmodality ( b ) ) \add ( #se1 = TRUE ==> ) ;
"Assertion (#se1) Failure" : \replacewith ( \modality{#allmodal}{.. throw new java.lang.AssertionError(#se2); ...}\endmodality ( b ) ) \add ( #se1 = FALSE ==> )
\heuristics (simplify_prog )
\displayname "assert"
};defined in: assertions.key Line: 56 Offset :4assertWithReferenceMessageNull {
\find ( \modality{#allmodal}{.. assert #se1 : null; ...}\endmodality ( b ) )
"Assertion (#se1) OK" : \replacewith ( \modality{#allmodal}{.. ...}\endmodality ( b ) ) \add ( #se1 = TRUE ==> ) ;
"Assertion (#se1) Failure" : \replacewith ( \modality{#allmodal}{..
throw new java.lang.AssertionError((java.lang.Object)null); ...}\endmodality ( b ) ) \add ( #se1 = FALSE ==> )
\heuristics (simplify_prog )
\displayname "assert"
};defined in: assertions.key Line: 67 Offset :4assertWithPrimitiveMessage {
\find ( \modality{#allmodal}{.. assert #se1 : #se2; ...}\endmodality ( b ) )
\varcond "Assertion (#se1) OK" : \replacewith ( \modality{#allmodal}{.. ...}\endmodality ( b ) ) \add ( #se1 = TRUE ==> ) ;
"Assertion (#se1) Failure" : \replacewith ( \modality{#allmodal}{.. throw new java.lang.AssertionError(#se2); ...}\endmodality ( b ) ) \add ( #se1 = FALSE ==> )
\heuristics (simplify_prog )
\displayname "assert"
};defined in: assertions.key Line: 78 Offset :4skipAssert {
\find ( \modality{#allmodal}{.. assert #e1 : #e2; ...}\endmodality ( b ) )
\replacewith ( \modality{#allmodal}{.. ...}\endmodality ( b ) )
\heuristics (simplify_prog )
\displayname "skip assert"
};defined in: assertions.key Line: 92 Offset :4skipAssert_2 {
\find ( \modality{#allmodal}{.. assert #e1; ...}\endmodality ( b ) )
\replacewith ( \modality{#allmodal}{.. ...}\endmodality ( b ) )
\heuristics (simplify_prog )
\displayname "skip assert"
};defined in: assertions.key Line: 99 Offset :4assertSafe {
\schemaVar \variable Field f ;
\schemaVar \variable java.lang.Object o ;
\schemaVar \skolemTerm Heap oldHeap ;
\find ( ==> \modality{#allmodal}{.#ex.. assert #e1; ...}\endmodality ( b ) )
\varcond "Assertion (#e1) Skip" : \replacewith ( ==> \modality{#allmodal}{.. ...}\endmodality ( b ) ) ;
"Assertion (#e1) Terminates And OK" : \replacewith ( ==> \<{method-frame(#ex):{#condition = #e1;}}\> #condition = TRUE ) ;
"Assertion (#e1) No Effects" : \replacewith ( ==> \[{ method-frame(#ex):{
#typeof(#e1) #condition = #e1 ;
}
}\] ( \forall f ; \forall o ; ( ( o != null & select <[ boolean ]> ( oldHeap , o , java.lang.Object #$created ) = FALSE ) | select <[ any ]> ( oldHeap , o , f ) = select <[ any ]> ( heap , o , f ) ) ) ) \add ( oldHeap = heap ==> )
\heuristics (simplify_prog )
\displayname "assert"
};defined in: assertions.key Line: 110 Offset :4assertSafeWithMessage {
\schemaVar \variable Field f ;
\schemaVar \variable java.lang.Object o ;
\schemaVar \skolemTerm Heap oldHeap ;
\find ( ==> \modality{#allmodal}{.#ex.. assert #e1 : #e2; ...}\endmodality ( b ) )
\varcond "Assertion (#e1) Skip" : \replacewith ( ==> \modality{#allmodal}{.. ...}\endmodality ( b ) ) ;
"Assertion (#e1) Terminates And OK" : \replacewith ( ==> \<{method-frame(#ex):{#typeof(#e1) #condition = #e1;
#typeof(#e2) #message = #e2;}}\> #condition = TRUE ) ;
"Assertion (#e1) No Effects" : \replacewith ( ==> \[{ method-frame(#ex):{
#typeof(#e1) #condition = #e1;
#typeof(#e2) #message = #e2;
}
}\] ( \forall f ; \forall o ; ( ( o != null & select <[ boolean ]> ( oldHeap , o , java.lang.Object #$created ) = FALSE ) | select <[ any ]> ( oldHeap , o , f ) = select <[ any ]> ( heap , o , f ) ) ) ) \add ( oldHeap = heap ==> )
\heuristics (simplify_prog )
\displayname "assert"
};defined in: assertions.key Line: 131 Offset :4