About Us Products Articles News Contact Support

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:

Example 2. - While loop:

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:

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

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

• “start” - the implicit beginning of the operation’s body, the only known is that x is not initialized.
• 1 - first numbered statement, assignment to x, which creates a new labeled version of this variable (obviously, this new version is considered to be initialized). The check in the right column verifies that the new value is within the type.
• 2 - this number corresponds to the top of the While statement (branch statements have further numbers) where the condition is verified for reachability - that is, it is expected that the loop will execute at least once. The condition refers to the latest version of x (which is x1) from before the loop.
• 3 - this is the incrementation of x in the loop body, where the usual arithmetic checks are performed, in both pre- and post- forms (this is why there are two rows in the table for this single index). It should be noted, however, that the last known version of x is now x2 - this is a deliberate abandoning of the history continuity. At this point the relation between x2 and x1 is not known - in other words, the fact that x1 was 0 before the loop has no influence on how x2 is treated within the loop. It is known, however, that x2 satisfies the type and the loop condition.
• 4 - this is the Assert statement already after the loop. The knowledge from the loop branch was propagated out in the form of the x4 version, which was statically determined to be the same as x3 (this is because the loop condition is trivially known to be satisfied by x1). The interesting thing, however, is that there is not enough knowledge about x4 to satisfy the assertion, as will be seen later.
• “finish” - the implicit end of the operations body, the check verifies that the local variable x was assigned on at least one execution path.

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:

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.