|
|
||
|
This article belongs to the series documenting the reasoning behind and development of new features in the Formal Methods Toolkit.
The previous article presented handling of loop invariants, with the following motivating example:
It was possible to prove that after this loop x has value 10, based on how the loop invariant is expanded. In particular (and as explained in the previous article), the following assumption is injected just after the loop:
This readily simplifies to x==10 in the set of knowns, which is what was intended.
The problem is - the above reasoning is correct from the logic point of view also when the loop does not terminate at all. The following programming error demonstrates the problem:
The meaning of loop invariant is still the same - the invariant holds across every iteration and as long as the loop exits due to its condition not being met, the assumption at the end is true. But the loop never terminates, because its controlling variable x is not modified due to programming error.
This problem can be solved by involving loop variants, which are expressions that are guaranteed to change monotonically in every iteration and hit some limit. The usual variant is something that is decremented in every iteration and yet non-negative, both of which guarantee that the loop must eventually terminate.
This concept can be expressed explicitly by the programmer with the help of additional variables, for example:
The variant expression is becoming smaller with each iteration and is non-negative, so the loop must terminate. With the programming error as before, the assert would fail.
Still, the above is not very convenient, because two new variables are needed. These variables are used only for proofs and there is no reason to retain them at run-time, which means that ghost variables might be a better solution here. But even then, ghost variables need to be announced at the system level, which is useful when there is a need to express relations between different operations, but wasteful in such local contexts.
In order to help solving problems like above, ad-hoc ghosts were introduced. They have temporary nature and do not need to be declared - instead they are managed on the fly with operations GhostCapture and GhostRecall, for example:
The GhostCapture operation stores an arbitrary expression, referring to variable versions that are active at the given location, under arbitrary string name - GhostRecall can be used to retrieve that expression later within the same operation. The only limitation for its use is that GhostRecall can be effectively used only in asserts and assumes. Moreover, both GhostCapture and GhostRecall are proof-only features and they are not translated into the final generated source code - and the captured expressions are valid only within the context of a single operation.
These ad-hoc ghost features can be used to solve different proof problems by referring to “older” forms of arbitrary expressions, but since their use with loop variants is so idiomatic, it was beneficial to simplify their use even further - the LoopVariant feature allows to wrap the above in a much simpler form:
The above allows to prove the correctness of the loop and detect programming errors that would prevent the loop from terminating.
Just for reference, the above readable code is internally expanded to the following form:
There can be none, one or multiple invariants and variants in the loop, introduced either by means of distinct LoopInvariant and LoopVariant elements in conjunction with the main loop condition, or by means of multiple arguments given to these elements. They are handled separately (that is, they are translated into separate asserts and assumes) with clean list of knowns and proof conditions in mind.
The GhostCapture, GhostRecall and LoopVariant features will be available in FMT 2.0.