|
|
||
|
This article belongs to the series documenting the reasoning behind and development of new features in the Formal Methods Toolkit.
The previously described Deduce and Induce features are important building blocks supporting the use of quantified statements, but they cannot be treated as complete solutions in isolation. In particular, both of them create new facts from existing quantified statements, which assumes that there are some existing statements in the first place. Previous examples used the Assume construct to provide something to start with (like in the case where the first array element is set according to some expected pattern), but assumptions are relatively dangerous since they introduce new knowns without verifying them. There are cases where such a heavy-handed tool is needed, but constructing the first quantified statement from a single array element does not justify its use - it is perfectly possible to verify whether the given statement is valid and the automated verification is one of the reasons why formal methods are introduced in the first place.
Continuing with the example of an operation that fills the array with zeros and where the first element was already assigned, the first quantified statement needs to have the following meaning:
where i==1 represents the single-element region, which can then be extended (with Induce) when subsequent array elements are assigned to.
It seems reasonable to keep the grammar simple and the number of special symbols small, so instead of introducing additional special form, the Induce operation was adopted for this purpose:
The meaning of this is that a quantified statement that is valid on an empty set is extended at the extension point i->1, which allows to construct a new statement with the intended meaning. The use of empty set symbol is intuitive here. Of course, the toolkit verifies whether the expression is indeed true at the point of extension (that is, whether a[[1]]==0) and rejects the induction if it is not the case.
The following is a complete example operating on the first 3 array elements:
The proof statements for the above operation show the accumulation of knowns in each step:
This table is relatively long, because even such a simple function can generate substantial amount of facts to analyze. What is important here is that the exact structure of region descriptions is not important, as long as they match in terms of coverage. Thus, even though the first region was specified as i==1, it was later automatically matched to 1<=i<=1, which was written as a matter of convention, as it nicely extends to larger regions. Ultimately, the last fact displayed in the table above is equivalent to:
This equivalence can be verified either with assertion at the end of the operation or with the post-condition defined at the time of declaration. The revised example, with post-condition added in the operation declaration is:
The above result shows that all proof conditions were discharged successfully.
It is reasonable to expect the features presented above to be reused within loop invariants. Future articles in this series will describe the challenges and progress in implementing support for such constructs.