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 ;
\schemaVar \program [ list ] Statement #localVarDeclsBefore_LOOP ;
\schemaVar \update #updateBefore_LOOP ;
\schemaVar \update #updateFrame_LOOP ;
\find ( ( \modality{#dia} {.. while (#nse) #body ... }\endmodality ( post ) ) )
\varcond \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;
#localVarDeclsBefore_LOOP
}\endmodality ( { #createBeforeLoopUpdate ( loopFormula , #heapBefore_LOOP , #savedHeapBefore_LOOP , #permissionsBefore_LOOP ) || #updateBefore_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 & { #updateFrame_LOOP } #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 ;
\schemaVar \program [ list ] Statement #localVarDeclsBefore_LOOP ;
\schemaVar \update #updateBefore_LOOP ;
\schemaVar \update #updateFrame_LOOP ;
\find ( ( \modality{#box} {.. while (#nse) #body ... }\endmodality ( post ) ) )
\varcond \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;
#localVarDeclsBefore_LOOP
}
\endmodality ( { #createBeforeLoopUpdate ( loopFormula , #heapBefore_LOOP , #savedHeapBefore_LOOP , #permissionsBefore_LOOP ) || #createLocalAnonUpdate ( loopFormula ) || #updateBefore_LOOP || #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 & { #updateFrame_LOOP } #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: 121 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: 201 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 ;
\schemaVar \program [ list ] Statement #localVarDeclsBefore_LOOP ;
\schemaVar \update #updateBefore_LOOP ;
\schemaVar \update #updateFrame_LOOP ;
\find ( ( \modality{#dia} {.. while (#nse) #body ... }\endmodality ( post ) ) )
\varcond \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;
#localVarDeclsBefore_LOOP
}
\endmodality ( { #createBeforeLoopUpdate ( loopFormula , #heapBefore_LOOP , #savedHeapBefore_LOOP , #permissionsBefore_LOOP ) || #createLocalAnonUpdate ( loopFormula ) || #updateBefore_LOOP || #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 & { #updateFrame_LOOP } #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: 233 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 ;
\schemaVar \program [ list ] Statement #localVarDeclsBefore_LOOP ;
\schemaVar \update #updateBefore_LOOP ;
\schemaVar \update #updateFrame_LOOP ;
\find ( ( \modality{#box} {.. while (#nse) #body ... }\endmodality ( post ) ) )
\varcond \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;
#localVarDeclsBefore_LOOP
}
\endmodality ( { #createBeforeLoopUpdate ( loopFormula , #heapBefore_LOOP , #savedHeapBefore_LOOP , #permissionsBefore_LOOP ) || #createLocalAnonUpdate ( loopFormula ) || #updateBefore_LOOP || #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 & { #updateFrame_LOOP } #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: 351 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: 458 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: 470 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: 501 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: 507 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: 513 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: 519 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: 529 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: 535 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: 541 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: 547 Offset :4