Inspirel banner

Fixing Loops

This article belongs to the series documenting the reasoning behind and development of new features in the Formal Methods Toolkit.

The While loop and If statement have the same structure from the grammar perspective and both are considered to be conditional statements within the FMT tool, although there is an important difference between them that has an impact on how proof statements are generated.

The following two examples allow to bring that difference into focus.

Example 1. - If statement:

Image

Example 2. - While loop:

Image

Even though both code fragments are very similar, and both are conditional in nature, the information flow is different. In the If example the body of the conditional statement can rely on the known the was established before (that is, x having value 0), and it is therefore possible to compute that at the end of the branch x will be 1. It is also possible to state that after the If statement x will be 1, too, because the known generated within the branch can propagate out, as the condition is statically known to be True. Neither of these two reasoning paths are possible with While - the knowns from before the statement are not meaningful in all loop iterations, so the proof statements within the branch should be created without continuity of history of variable modifications.

The implementation in the 1.0 version of FMT did not take this subtlety into account. The corrected handling of loop proof statements is demonstrated in the following FMT session:

Image
Image
Image
Image

The following table shows the accumulation of knowns in each step:

Image
Image

There is a lot of information in this table and it is worth to explain each row separately:

The most important part of this example is the discontinuity of history between the context before and within the loop. This is achieved by implicitly unrolling the loop once and generating the proof statements as if the loop started from its second iteration, abandoning the knowns from the first run. This is how x2 came into being; the type invariants and its initialization flags are added artificially.

The missing part is the retention of knowledge across the loop - it is obvious for the human engineer that at the end of the operation x has value 10, however:

Image
Image

In order to close this gap the system needs to be extended with support for loop invariants. This will be addressed in later articles. In any case, the corrected handling of loops will be available in FMT 2.0.