Sunday, October 02, 2022

Infinity and verification of Z++ Compiler

With regard to Z++ compiler, input is a set of Z++ source/header files, and output is a single Z++ executable file. Regardless of the input mechanism (keyboard, mouse, touch, etc.), a piece of software receives an input, and produces an output (text, GUI, speaks the result, etc.). The purpose of testing is to determine whether the output is as expected for any given input. For the process of engineering, this cannot be proven. The only means we have is testing.

Consider a newly built passenger plane. All engineers can show you precise measurements, like power of the engines, span of wings, and so on. Yet, you would not want to be the first passenger on the plane. That is because, while putting the plane together someone could have made a mistake. For instance, a screw did not receive the intended torque. The process of engineering is not mathematical, hence cannot be proven to be correct, or otherwise.

Software engineering is also an engineering process. For instance, an object may be initialized incorrectly. In particular, an algorithm and its implementation are not the same thing, just as an engineer's design and measurements for a plane is not the same as the product made according to the design.

Going back to testing Z++ compiler, we immediately notice that the input set is infinite. Well, let us make that clear. After all, what is infinite and how do we deal with it? Following this digression is not necessary to understand the point of the article but is needed for completion.

Consider the 10 digits, 0, 1, ...9 introduced by Kharazmi in his book of algebra. With these, few symbols we can make an infinite set of symbols. That is because, regardless of what number is written down, we can always add one to it, thereby making a bigger one. So, our first observation is that a finite set can be used to make an infinite set.

Galileo noticed that there are as many multiples of 5 (5, 10, 15, ...) as the counting numbers, 1, 2, 3, ....  He only wrote that down in the corner of some book but never disclosed it. It was an odd observation where a part of something is the same the thing itself. Actually, Euclid a long-time earlier had shown that the set of prime numbers is infinite. Our second observation is that an infinite set contains infinitely many infinite subsets.

Note that, the notion of infinity is a mathematical concept. Nothing in existence is infinite. Not even the set of universes in a multiverse view. But that is not relevant to our topic of discussion. Just imagine what would happen if the set of counting numbers were finite. How could we write down the next Federal Budget Deficit!

We need one more concept, that of independence, or orthogonality. Given a plane, as in Euclidean geometry, we can make two perpendicular unit vectors, whose extensions are known as the x-axes and the y-axis. Now, any vector in the plane can be described in terms of these two vectors, via coordinates. However, if you pick a point outside of the plane, you cannot describe it. You will need a third unit vector perpendicular to the plane of the first two. This third unit vector is independent of the previous two and makes an infinite space that contains the plane (which is infinite).

It is not straightforward to explain how an independent set of Z++ programs can be selected. For now, assume that has been done. So, we have a finite set of independent Z++ programs. We know this will generate an infinite set of Z++ programs, e.g. like the two axis of a plane. So, if we test and show that this finite set works fine, then we have shown that an infinite set works fine, too.

Of course, our infinite set will not cover the entire set of possible Z++ programs. In the future, someone will write a Z++ program which may produce incorrect output. That means we have found a Z++ program that is independent from our finite selected set of Z++ program. We will add that to our test set and fix the problem. As we continue to do that, we will make the infinite set of correctly working Z++ programs (intuitively speaking) larger (well, notice that we cannot say bigger infinite, except in a different mathematical sense which we will not mention here).

So, what do we have. Well, is a passenger plane really tested for all possible conditions that it may go through? It only needs to be tested for a well-selected set of conditions. Accordingly, if the finite set of Z++ programmers that we have selected is a good representative of all the useful programs that could be written, we have successfully verified Z++ Compiler.

The purpose of this article is to clarify that software cannot be proven correct and must be tested. The selected set of test examples is finite and independent. That, we will never be able to show that there are no further issues that we need to fix. So long as we are able to select a finite set that represents most possible uses, and show that set works fine, we have demonstrated the validity of the software.

By the way, the purpose of independence is to keep the finite selected test set small. Even as such, the test set for Z++ compiler is about a thousand, possibly with some redundant examples.


Labels: , , , , ,