The problem with programs

Recently at my work I have been fortunate enough to go on several courses to further my understanding. Being a company that is concerned primarily with producing safety critical software, we have to consider certain things more carefully when we are writing our code. The desire is that our solution does exactly what the customer wants and nothing else. This presents several interesting problems, the most interesting of which is that of determining exactly what the customer wants. A normal English language document is bound to be full of ambiguities, either caused by the poetic nature of our tongue or due to cases that have simply been omitted. It is all too common for one specific set of conditions to be missed, either because the author deems it obvious what should happen or it doesn’t seem important to them. However, when it comes to designing a system that has to be safe for all users at all times, its behaviour has to be clearly defined.

The level of clarity however is open to debate among computer scientists, as the more rigorously defined your system is, the less freedom the programmers have to edit the design. This can be a good thing but could also lead to developers having a sore deal. You can subsequently miss optimisations that only a computer programmer would spot and the system designer would not comprehend.

In my office we aim to avoid writing ambiguous requirements in the specification at all cost. This is done by not writing in plain English, but instead using a formal specification language such as Z to express the desirable qualities of the system. Z is a very interesting concept and one that I thoroughly enjoy. It consists of two parts, a mathematical description of the function required and an English explanation thereof. The aim is to mathematically define all the things we care about so that there is no other interpretation than the correct one.

To show what I mean and how it works, let us consider an example. Consider the following function definition:

The matching function will take an integer and a word as input and if the word is as long as the number input or the written form of the integer, then it returns true, else false.

At first glance, this seems obvious and clear, but there are some ambiguities present. What word is used to represent 0, or is there more than one? Is the or condition an exclusive or; should four and 4 return false or, as one would suspect, true? How big an integer are we allowed, and what is the maximum length of a word that we can store when we come to write this program? This is why mathematics is used, to make sure all things have a clearly defined exclusive definition. In Z, the above definition would be acceptable if accompanied by what in the language is called a schema. This would either use (or) or (xor) to show which was intended, and thereby ensure that the real meaning was clear. There would also be a function defining exactly what words mapped to a number and all types would be very clearly defined with their range specified.

The process of turning the English into mathematics does fascinate me and is something I feel could be used elsewhere too. I think that mystery in language is a beautiful thing, but that it can be counterproductive in some instances. For example, the law in England is very ambiguous and the courts time is often filled with debate on the intended meaning of certain words. The aim of those writing it is that it will be clear exactly when an infringement has occurred, but it is not the case. I believe mathematics could seriously help with this problem. I agree that it would take a long time to convert it and people would need to be educated in the formal specification language to ensure they were able to understand the regulations they were trying to follow, but overall I feel it would be worth it. I would certainly use mathematical laws if I was on a dessert island, and a clearly defined system of sentencing too.

That point aside, I hope to have introduced to you the concept of formal specification. For me, it unites my fascinations of language and mathematics which previously seemed to conflict but now unite. I know there is debate among scientists as to whether mathematics is a language or a real entity, but it can most certainly be used as a language. It may not have the poetry and imagery that English can concoct, but it has an elegance and precise simplicity that makes it beautiful. If you want to know more, there are plenty of sites on the internet that can help, or I have a book if you wish to borrow it. I hope to at least have informed you of what maths is possible of.