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 ))
\sameUpdateLevel
"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 ))
\sameUpdateLevel
\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: 57 Offset :4assertWithReferenceMessageNull {
\find ( \modality{#allmodal}{.. assert #se1 : null; ...}\endmodality ( b ))
\sameUpdateLevel
"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: 69 Offset :4assertWithPrimitiveMessage {
\find ( \modality{#allmodal}{.. assert #se1 : #se2; ...}\endmodality ( b ))
\sameUpdateLevel
\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: 81 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: 96 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: 103 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 & boolean :: select ( oldHeap , o , java.lang.Object :: )= FALSE )| any :: select ( oldHeap , o , f )= any :: select ( heap , o , f )))) \add ( oldHeap = heap ==> )
\heuristics (simplify_prog )
\displayname "assert"
};defined in: assertions.key Line: 114 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 & boolean :: select ( oldHeap , o , java.lang.Object :: )= FALSE )| any :: select ( oldHeap , o , f )= any :: select ( heap , o , f )))) \add ( oldHeap = heap ==> )
\heuristics (simplify_prog )
\displayname "assert"
};defined in: assertions.key Line: 135 Offset :4