loopScopeRules.key
Taclets
Enabled under choices:
programRules:JavajavaLoopTreatment:efficient
loopScopeInvDia
loopScopeInvDia {
\schemaVar \formula inv ;
\schemaVar \formula freeInv ;
\schemaVar \term any variantTerm ;
\schemaVar \formula loopFormula ;
\schemaVar \program Statement #loopStmt;
\schemaVar \program Variable #variant;
\schemaVar \skolemTerm Heap anon_heap_LOOP ;
\schemaVar \skolemTerm Heap anon_savedHeap_LOOP ;
\schemaVar \skolemTerm Heap anon_permissions_LOOP ;
\schemaVar \program Variable #heapBefore_LOOP;
\schemaVar \program Variable #savedHeapBefore_LOOP;
\schemaVar \program Variable #permissionsBefore_LOOP;
\find ( ( \modality{#dia} {.. while (#nse) #body ... }\endmodality ( post )))
\varcond \varcond \varcond \varcond \varcond \varcond \varcond \varcond \varcond \varcond \varcond "Invariant Initially Valid" : \replacewith ( inv );
"Invariant Preserved and Used" : \replacewith ( \modality{#dia}{
#typeof(#heapBefore_LOOP) #heapBefore_LOOP;
#typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP;
#typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP;
#typeof(#variant) #variant;
}\endmodality ( { #createBeforeLoopUpdate ( loopFormula , #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)|| #createLocalAnonUpdate ( loopFormula )|| #createHeapAnonUpdate ( loopFormula , anon_heap_LOOP , anon_savedHeap_LOOP , anon_permissions_LOOP )} { #variant:= variantTerm } ( inv & freeInv -> ( \modality{#dia}{
..
boolean #x;
loop-scope(#x) {
if (#nse) {
#body
continue;
} else {
break;
}
}
...
}\endmodality ( ( #x<< loopScopeIndex >> = TRUE -> post )& ( #x<< loopScopeIndex >> = FALSE -> inv & #createFrameCond ( loopFormula , #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)& prec ( variantTerm , #variant))))))) \add ( #wellFormedCond ( loopFormula , anon_heap_LOOP , anon_savedHeap_LOOP , anon_permissions_LOOP )==> )
\heuristics (loop_scope_inv_taclet )
};defined in: loopScopeRules.key Line: 26 Offset :4
loopScopeInvBox
loopScopeInvBox {
\schemaVar \formula inv ;
\schemaVar \formula freeInv ;
\schemaVar \formula loopFormula ;
\schemaVar \program Statement #loopStmt;
\schemaVar \skolemTerm Heap anon_heap_LOOP ;
\schemaVar \skolemTerm Heap anon_savedHeap_LOOP ;
\schemaVar \skolemTerm Heap anon_permissions_LOOP ;
\schemaVar \program Variable #heapBefore_LOOP;
\schemaVar \program Variable #savedHeapBefore_LOOP;
\schemaVar \program Variable #permissionsBefore_LOOP;
\find ( ( \modality{#box} {.. while (#nse) #body ... }\endmodality ( post )))
\varcond \varcond \varcond \varcond \varcond \varcond \varcond \varcond \varcond "Invariant Initially Valid" : \replacewith ( inv );
"Invariant Preserved and Used" : \replacewith ( \modality{#box}{
#typeof(#heapBefore_LOOP) #heapBefore_LOOP;
#typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP;
#typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP;
}
\endmodality ( { #createBeforeLoopUpdate ( loopFormula , #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)|| #createLocalAnonUpdate ( loopFormula )|| #createHeapAnonUpdate ( loopFormula , anon_heap_LOOP , anon_savedHeap_LOOP , anon_permissions_LOOP )} ( inv & freeInv -> ( \modality{#box}{
..
boolean #x;
loop-scope(#x) {
if (#nse) {
#body
continue;
} else {
break;
}
}
...
}\endmodality ( ( #x<< loopScopeIndex >> = TRUE -> post )& ( #x<< loopScopeIndex >> = FALSE -> inv & #createFrameCond ( loopFormula , #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP))))))) \add ( #wellFormedCond ( loopFormula , anon_heap_LOOP , anon_savedHeap_LOOP , anon_permissions_LOOP )==> )
\heuristics (loop_scope_inv_taclet )
};defined in: loopScopeRules.key Line: 107 Offset :4
Taclets
Enabled under choices:
programRules:Java
unwindLoopScope
unwindLoopScope {
\find ( ( \modality{#allmodal} {.. while (#nse) #body ... }\endmodality ( post )))
\varcond \replacewith ( ( \modality{#allmodal} {..
boolean #x;
loop-scope(#x) {
if (#nse) { #body continue; }
else { break; }
}
... }
\endmodality ( ( #x<< loopScopeIndex >> = TRUE -> post )& ( #x<< loopScopeIndex >> = FALSE -> ( \modality{#allmodal} {..
#reattachLoopInvariant(while (#nse) #body);
... }\endmodality ( post ))))))
\heuristics (loop_scope_expand )
};defined in: loopScopeRules.key Line: 177 Offset :4
Taclets
Enabled under choices:
programRules:JavajavaLoopTreatment:teaching
threeBranchLoopScopeInvRuleDia
threeBranchLoopScopeInvRuleDia {
\schemaVar \formula inv ;
\schemaVar \formula freeInv ;
\schemaVar \term any variantTerm ;
\schemaVar \formula loopFormula ;
\schemaVar \program Statement #loopStmt;
\schemaVar \program Variable #variant;
\schemaVar \skolemTerm Heap anon_heap_LOOP ;
\schemaVar \skolemTerm Heap anon_savedHeap_LOOP ;
\schemaVar \skolemTerm Heap anon_permissions_LOOP ;
\schemaVar \program Variable #heapBefore_LOOP;
\schemaVar \program Variable #savedHeapBefore_LOOP;
\schemaVar \program Variable #permissionsBefore_LOOP;
\find ( ( \modality{#dia} {.. while (#nse) #body ... }\endmodality ( post )))
\varcond \varcond \varcond \varcond \varcond \varcond \varcond \varcond \varcond \varcond \varcond "Invariant Initially Valid" : \replacewith ( inv );
"Body Preserves Invariant" : \replacewith ( \modality{#dia}{
#typeof(#heapBefore_LOOP) #heapBefore_LOOP;
#typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP;
#typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP;
#typeof(#variant) #variant;
}
\endmodality ( { #createBeforeLoopUpdate ( loopFormula , #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)|| #createLocalAnonUpdate ( loopFormula )|| #createHeapAnonUpdate ( loopFormula , anon_heap_LOOP , anon_savedHeap_LOOP , anon_permissions_LOOP )} { #variant:= variantTerm } ( inv & freeInv -> ( \modality{#dia}{
..
boolean #x;
loop-scope(#x) {
if (#nse) {
#body
continue;
} else {
break;
}
}
...
}\endmodality ( #x<< loopScopeIndex >> = FALSE -> inv & #createFrameCond ( loopFormula , #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)& prec ( variantTerm , #variant)))))) \add ( #wellFormedCond ( loopFormula , anon_heap_LOOP , anon_savedHeap_LOOP , anon_permissions_LOOP )==> );
"Use Case" : \replacewith ( \modality{#dia}{
#typeof(#heapBefore_LOOP) #heapBefore_LOOP;
#typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP;
#typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP;
#typeof(#variant) #variant;
}
\endmodality ( { #createBeforeLoopUpdate ( loopFormula , #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)|| #createLocalAnonUpdate ( loopFormula )|| #createHeapAnonUpdate ( loopFormula , anon_heap_LOOP , anon_savedHeap_LOOP , anon_permissions_LOOP )} { #variant:= variantTerm } ( inv & freeInv -> ( \modality{#dia}{
..
boolean #x;
loop-scope(#x) {
if (#nse) {
#body
continue;
} else {
break;
}
}
...
}\endmodality ( #x<< loopScopeIndex >> = TRUE -> post ))))) \add ( #wellFormedCond ( loopFormula , anon_heap_LOOP , anon_savedHeap_LOOP , anon_permissions_LOOP )==> )
\heuristics (loop_scope_inv_taclet )
};defined in: loopScopeRules.key Line: 209 Offset :4
threeBranchLoopScopeInvRuleBox
threeBranchLoopScopeInvRuleBox {
\schemaVar \formula inv ;
\schemaVar \formula freeInv ;
\schemaVar \formula loopFormula ;
\schemaVar \program Statement #loopStmt;
\schemaVar \skolemTerm Heap anon_heap_LOOP ;
\schemaVar \skolemTerm Heap anon_savedHeap_LOOP ;
\schemaVar \skolemTerm Heap anon_permissions_LOOP ;
\schemaVar \program Variable #heapBefore_LOOP;
\schemaVar \program Variable #savedHeapBefore_LOOP;
\schemaVar \program Variable #permissionsBefore_LOOP;
\find ( ( \modality{#box} {.. while (#nse) #body ... }\endmodality ( post )))
\varcond \varcond \varcond \varcond \varcond \varcond \varcond \varcond \varcond "Invariant Initially Valid" : \replacewith ( inv );
"Body Preserves Invariant" : \replacewith ( \modality{#box}{ #typeof(#heapBefore_LOOP) #heapBefore_LOOP;
#typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP;
#typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP;
}
\endmodality ( { #createBeforeLoopUpdate ( loopFormula , #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)|| #createLocalAnonUpdate ( loopFormula )|| #createHeapAnonUpdate ( loopFormula , anon_heap_LOOP , anon_savedHeap_LOOP , anon_permissions_LOOP )} ( inv & freeInv -> ( \modality{#box}{
..
boolean #x;
loop-scope(#x) {
if (#nse) {
#body
continue;
} else {
break;
}
}
...
}\endmodality ( #x<< loopScopeIndex >> = FALSE -> inv & #createFrameCond ( loopFormula , #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)))))) \add ( #wellFormedCond ( loopFormula , anon_heap_LOOP , anon_savedHeap_LOOP , anon_permissions_LOOP )==> );
"Use Case" : \replacewith ( { #createBeforeLoopUpdate ( loopFormula , #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)|| #createLocalAnonUpdate ( loopFormula )|| #createHeapAnonUpdate ( loopFormula , anon_heap_LOOP , anon_savedHeap_LOOP , anon_permissions_LOOP )} ( inv & freeInv -> ( \modality{#box}{
..
boolean #x;
loop-scope(#x) {
if (#nse) {
#body
continue;
} else {
break;
}
}
...
}\endmodality ( #x<< loopScopeIndex >> = TRUE -> post )))) \add ( #wellFormedCond ( loopFormula , anon_heap_LOOP , anon_savedHeap_LOOP , anon_permissions_LOOP )==> )
\heuristics (loop_scope_inv_taclet )
};defined in: loopScopeRules.key Line: 317 Offset :4
Taclets
Enabled under choices:
programRules:Java
lsBreak
lsBreak {
\find ( \modality{#allmodal}{.. loop-scope(#lhs) { break; #slist } ...}\endmodality ( post ))
\replacewith ( \modality{#allmodal}{.. #lhs = true; ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: loopScopeRules.key Line: 414 Offset :4
lsContinue
lsContinue {
\find ( \modality{#allmodal}{.. loop-scope(#lhs) { continue; #slist } ...}\endmodality ( post ))
\replacewith ( { #lhs:= FALSE } post )
\heuristics (simplify_prog )
};defined in: loopScopeRules.key Line: 420 Offset :4
lsLblContinueMatch
lsLblContinueMatch {
\find ( \modality{#allmodal}{.. #lb: loop-scope(#lhs) { continue #lb; #slist } ...}\endmodality ( post ))
\replacewith ( { #lhs:= FALSE } post )
\heuristics (simplify_prog )
};defined in: loopScopeRules.key Line: 426 Offset :4
lsLblContinueNoMatch2
lsLblContinueNoMatch2 {
\schemaVar \program Statement #lsStmt;
\find ( \modality{#allmodal}{.. #lb1: loop-scope(#lhs) { continue #lb; #slist } ...}\endmodality ( post ))
\varcond \replacewith ( \modality{#allmodal}{.. #lhs = true; continue #lb; ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: loopScopeRules.key Line: 447 Offset :4
lsLblBreak
lsLblBreak {
\find ( \modality{#allmodal}{.. loop-scope(#lhs) { break #lb; #slist } ...}\endmodality ( post ))
\replacewith ( \modality{#allmodal}{.. { #lhs = true; break #lb; } ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: loopScopeRules.key Line: 457 Offset :4
lsThrow
lsThrow {
\find ( \modality{#allmodal}{.. loop-scope(#lhs) { throw #se; #slist } ...}\endmodality ( post ))
\replacewith ( \modality{#allmodal}{.. #lhs = true; throw #se; ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: loopScopeRules.key Line: 463 Offset :4
lsReturnNonVoid
lsReturnNonVoid {
\find ( \modality{#allmodal}{.. loop-scope(#lhs) { return #se; #slist } ...}\endmodality ( post ))
\replacewith ( \modality{#allmodal}{.. #lhs = true; return #se; ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: loopScopeRules.key Line: 469 Offset :4
lsReturnVoid
lsReturnVoid {
\find ( \modality{#allmodal}{.. loop-scope(#lhs) { return; #slist } ...}\endmodality ( post ))
\replacewith ( \modality{#allmodal}{.. #lhs = true; return; ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: loopScopeRules.key Line: 475 Offset :4
blockContinue
blockContinue {
\find ( \modality{#allmodal}{.. { continue; #slist } ...}\endmodality ( post ))
\replacewith ( \modality{#allmodal}{.. continue; ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: loopScopeRules.key Line: 485 Offset :4
blockBreak
blockBreak {
\find ( \modality{#allmodal}{.. { break; #slist } ...}\endmodality ( post ))
\replacewith ( \modality{#allmodal}{.. break; ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: loopScopeRules.key Line: 491 Offset :4
blockContinueLabeled
blockContinueLabeled {
\find ( \modality{#allmodal}{.. { continue #lb; #slist } ...}\endmodality ( post ))
\replacewith ( \modality{#allmodal}{.. continue #lb; ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: loopScopeRules.key Line: 497 Offset :4
blockBreakLabeled
blockBreakLabeled {
\find ( \modality{#allmodal}{.. { break #lb; #slist } ...}\endmodality ( post ))
\replacewith ( \modality{#allmodal}{.. break #lb; ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: loopScopeRules.key Line: 503 Offset :4