Supporting Quantified Statements - Part 1
This article belongs to the series documenting the reasoning behind and development of new features in the Formal Methods Toolkit.
Quantified statements are very powerful tools in the area of formal methods, as they allow to express (and verify) knowledge that binds together multiple elements. Quantified statements involve existential and universal quantifiers and allow to state things such as:
- There exists an element in the collection that has some property of interest. The exact location of the given element might not be known, but the bare fact that it exists might be already important. For example: there is an entry for John in the phonebook. It is therefore known that an operation that searches for John in the phonebook will certainly succeed.
- All elements in the collection have some property of interest. For example, an operation that initializes elements of some array could promise that when it finishes, all elements are initialized. It is therefore known that no matter which element is accessed later on, it is certainly initialized.
- As another, more elaborate example, quantifiers allow to express the fact that some array is sorted or that some properties of the whole array are preserved during processing. They can also state that there is exactly one entry for John in the phonebook, which is stricter than the previous example.
In other words, quantified statements are essential for expressing requirements and for proving correctness of programs that deal with arrays, which are the most straightforward collections of objects treated together. Still, they were not supported in the first FMT release - this article sketches the ideas on what kind of support is needed.
Even though Mathematica recognizes both Exists and ForAll symbols (with very nice formatting), they are not automatically understood in all contexts and some work is necessary to integrate them with the existing FMT framework. The most fundamental building blocks are:
- The possibility to state that some quantified statement is true. This can have the form of type invariants, operation pre-conditions or assumptions.
- The possibility to verify that a given quantified statement is true. This can have the form of operation post-conditions or assertions.
- The possibility to induce new statements from existing ones. In particular, it should be possible to extend or shrink the range of some given statement when consecutive elements are processed. For example, in the context of universal quantifiers, if it is already known that all elements from 1 to 9 were processed and the element 10 was just processed as well, then it can be concluded that all elements from 1 to 10 were processed - which creates a new statement with wider scope. The existential quantifiers can benefit from this, too - for example, if it is known that there exists some interesting element of the array in the index range from 1 to 10, but it was just checked that element 1 is not the one in question, then a new, narrower statement can be created that the interesting range is from 2 to 10, which narrows the scope for further search. This inductive process, in both cases, is essential for proving correctness of loops, although it can be used outside of loops as well.
- The possibility to deduce individual facts from existing quantified statements. For example, it should be possible to conclude that the 5th element of the array has some property if it is already known that all elements from 1 to 10 have that property. That is, just as induction allows to build quantified statements from individual facts, deduction allows to extract individual facts from quantified statements.
- Considering the way in which FMT handles object assignments, where new numbered versions of assigned objects are created after each modification, there should also exist a mechanism for recreating quantified statements from old to new versions, taking into account the character of each modification. For example, when whole arrays are assigned to each other, the newly assigned array can acquire all quantified statements of the original array. Things are more complex when just a single element of the array is modified - in this case, the universal quantifier can be recreated with the scope reduced to omit the modified element, while the existential quantifier can be recreated conditionally, if the modified element is outside of the original scope.
Further articles in this mini-series will demonstrate the integration of these features in the FMT framework.
