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.


4 thoughts on “The problem with programs

  1. Maths when applied and actually used is amazing. Theoretical maths that is used just for the basis of having maths for something is boring, as are the theories that go with it.

    I still love using maths for stuff and actually think I’d probably enjoy working with the specifications you do. Maths is underrated

  2. chrysalisloall

    Yes, I think you would. I wish I could be involved in writing them and I may be able to in future.

    I only find some applied maths amazinf. For example, maths used to calculate aircraft trajectories and intersections, which I have to deal with, is dull to me. I honestly prefer the abstract stuff, like how can you measure how good this algorithm is? I think that’s part of me in general though, as I only rarely like anything concrete and applied. I’d much rather an abstract theory that will never help anyone over a specific problem, like the number of sofas we can fit in out living room. It may not be particularly useful, but it is more interesting. In my opinion anyway.

  3. I defintiely agree there has to be some level of interest in the outcome of the maths, otherwise its a tedious number crunch. The interest doesn’t necessarily have to be a valuable result though. It can be an equally absurd interest. It’s still applied maths over theoretical maths.

    Theoretical maths is the stuff I did at Uni which dealt with random sets of numbers and organising them and people theories on the best ways to do so. It was just badly written essays on why you use the equations you use. That’s what I was saying was boring.

  4. Chris

    Unfortunately when I was learning about formal methods and Z I had one of the many worlds most boring lecturers so unfortunately didn’t entirely get it. Though that may have something to do with playing a game on my phone during every one of his lectures … how I managed to get a good mark in that course is anyone’s guess.

    I definitely use maths quite a lot, and find it very helpful. In many ways it massively simplifies something which would otherwise be very complicated. It’s just a shame that they don’t tend to teach applied maths in school very well. I remember doing GCSE and finding it very boring but then when I got to A-level maths (which is a lot more applied than the theoretical boredom of GCSE) I really started to get it, understood why it was good and how it could make like life easier.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s