loopRules.key

Taclets

Enabled under choices: programRules:Java

loopUnwind

loopUnwind  {
\find (          \modality{#allmodal}{.. while(#e) #s ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #unwind-loop (#innerLabel, #outerLabel,
                while(#e) #s); ...}\endmodality            (                   post ))
\heuristics  (loop_expand )

};

defined in: loopRules.key Line: 29 Offset :4

doWhileUnwind

doWhileUnwind  {
\find (          \modality{#allmodal}{.. do #s while (#e); ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #unwind-loop (#innerLabel, #outerLabel, do #s while(#e);); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: loopRules.key Line: 37 Offset :4

for_to_while

for_to_while  {
\find (          \modality{#allmodal}{.. #forloop ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #for-to-while(#innerLabel, #outerLabel, #forloop) ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: loopRules.key Line: 48 Offset :4

arrayInitialisation

arrayInitialisation  {
\find (          \modality{#allmodal}{.#pm@#t(#a).. for (int #v=#se;#v           (                   post ))
  \replacewith (                {                  heap :=                 memset   (                   heap ,                    arrayRange   (                   #a,                    #se,                    length   (                   #a)-         1 ),                    #lit)} \modality{#allmodal}{..  ...}\endmodality            (                   post ))
\heuristics  (simplify )

};

defined in: loopRules.key Line: 55 Offset :4

KeY Logic Documentation