You are here: Home / Documentation / pipsmake-rc.htdoc / pipsmake-rc46.html

1PIPS design maps statement to decorations. For one loop statement, we need two transformers: one transformer to propagate the loop precondition as loop body precondition and a second transformer to propagate the loop precondition as loop postcondition. The second transformer can be deduced from the first one, but not the first one from the second one, and the second transformer is not used to compute the loop postcondition as it is more accurate to use the body postcondition. It is however computed to derive a compound statement transformer, e.g. the loop is part of block, which is part of a module statement, and then junked.

Document Actions

« October 2017 »
October
MoTuWeThFrSaSu
1
2345678
9101112131415
16171819202122
23242526272829
3031