15 - Formal reasoning

Summary

So far we have been using Z to name objects, describe their structure, and state some of their properties. For each property of an object, we added another formula to the description. But this is not always necessary. We don't have to spell out each property explicitly. Once we have stated a few properties, we can infer many more by using formal reasoning. This ability to infer new facts by applying simple rules is one of the distinguishing features of a formal method.

Reasoning enables us to use a formal model as a nonexecutable prototype or oracle. Formal reasoning plays somewhat the same role for mathematical models that testing does for code. Just as you can experiment with code by running it, you can investigate the behavior of a nonexecutable prototype by reasoning. You can check important system properties before you write a single line of code. Moreover, an exercise in formal reasoning often establishes the behavior for a whole class of situations, not just a single test case.

We can use formal reasoning to validate a mathematical model against requirements. A model is valid if its properties satisfy the intent of the requirements. Requirements are usually not expressed formally, but we can translate almost any reasonable requirement to a predicate. We can then attempt to determine whether this predicate follows from the predicates in our model. If it does, the model is valid with respect to that requirement.