The application of mathematically-derived techniques to software and hardware problems is commonly-resisted. There are a number of reasons for this - some of which have some substance and some of which do not. Such techniques - collectively called formal methods - have been heavily-promoted by their proponents for many years, but it is fair to say that their practical use is fairly limited. The areas where they have made some impact are generally quite specialised - and where the [perceived] extra effort is considered worthwile. For example, in safety-critical applications: more on these later. I say 'perceived' because many of the proponents of formal methods say that they do not really mean extra effort - formal methods mean more time and effort on the early phases of development (specification, design and so on) which is regained later because implementation is quicker, testing proceeds more smoothly, and maintenance is less of a problem. There is at least some truth in this, and a saying:
'We rushed the design to have more time building the implementation, to deal with the consequences of rushing the design.'
It is probably fair to say that rather than being an idea that will sweep the software industry from end to end, formal methods are one of many tools - which can be appropriately applied in certain circumstances. The remainder of this chapter is intended to explain why mathematics is sometimes necessary in software systems. But first an amusing story which is slightly relevant.
We tend to think of electrical communication networks as a modern concept, but they date back to the 19th Century. Samuel Morse, in the United States, invented Morse Code, which could be simply, quickly and reliably transmitted with very rudimentary equipment over very long distances. After the usual (and in hindsight) really stupid shortsightedness that follows such inventions (for example, the UK Admiralty did not see the point as it already had semaphore towers) telegraph systems spread rapidly.
Early systems consisted - as is still common today - of wires strung on poles. This is fine for crossing land and most rivers, but not larger bodies of water. The obvious solution is to simply lay the cable on the sea floor - which was first done across the English Channel. Unfortunately, it did not occur to anyone to insulate the cable, and - no big suprise - the bare wire in sea water did not work. Eventually though, submarine cable technology developed reliably: copper cable was surrounded by an insulater called Gutta Percha, a form of 'natural plastic' derived from trees in the Far East; the cable was then typically armoured by spiral wound iron wire. The amount of armour used depended on the precise use of the cable, and it had two roles: firstly it protected the cable in shallow water from (e.g.) fishing gear; and secondly it helped support the heavy cable when lowered in the ocean (potentially several kilometres deep).
There were, as is to be expected, a number of early fiascos - the funniest being the four attempts it took for an Anglo-French team to cross the Mediterranean from North to South. The first three failed.
The big cable laying task in the 19th Century was the Atlantic. The distance was vast, and there was no ship capable of carrying the cable. In 1857, the first attempt was made by an American consortium including Samuel Morse. Bear in mind that without a cable, setting up such a project took years (about three in fact). The ship problem was solved by converting two for cable laying, supplied by the UK and US governments: one British and one American (a certain amount of politics here probably). Contemporary engravings show the USS Niagra - a modern, for the time, warship, and the HMS Agammemnon, which looked like it had been at Trafalgar (because it had been at Trafalgar, over 60 years earlier - though a steam engine had been added). After one abortive attempt (the cable snapped about 300 miles offshore), they decided to sail to mid-Atlantic, join the cable, and sail home in opposite directions - the Niagra to Newfoundland, and the Agammemnon to Ireland - each laying cable as they went. Both ships were loaded with cable manufactured by different companies in the UK (no facilities were available in the US at the time).
When they reached mid-Atlantic, they found that the spiral armour on one was wound clockwise, and on the other anti-clockwise. This meant that it could not be properly spliced. So they improvised - and the cable actually worked for about a month.
The problem was a specification error - and I bet it is one that most of us would not have thought to check. Much of this module is about techniques that prevent such specification 'holes' - by forcing us to consider everything.
Incidentally, the first successful Atlantic cables were layed about 10 years later. Isambard Kindom Brunel's large liner The Great Eastern was a failure in its intended role, but was large enough to make a good cross-ocean cable layer. It was converted and used to lay the first trans-Atlantic cables. On the first attempt, the cable snapped (there were some metalurgical problems with the armour). Despite the depth (several kilometres) they dragged for and found the cable - but they did not have enough strong steel cable to bring it to the surface - their improvised collection of cables, ropes and chains kept breaking. They tried again with a second cable, this time successfully. And after that, they returned to the original cable, raised and repaired it, and continued to North America, so there were actually two cables - providing some welcome redundancy. The cables operated successfully for many years. The Great Eastern continued to operate as a cable-layer.
For many classes of computer system, reliability is a problem but not a critical problem. If your PC crashes (I mean of course when not if) then - provided you have taken some simple precautions - it should be just mildly irritating. However, there are other systems where failure cannot be tolerated.
The development of such systems obviously requires a higher level of attention than 'typical' software - and in many such systems it is appropriate to use formal methods. In practice, if you are developing software for the UK MoD, you have to use them for safety critical systems because the standards effectively require it. ('Effectively' means that the standards do not say 'use formal methods', they say 'use state of the art techniques'. This is for legal liability reasons essentially. There are other MoD standards that enable contractors to limit the amount of safety-critical code, so containing the problem.)
The term formal methods means the application of mathematically-derived techniques to the following.
Because natural language is simply not precise enough, we must use mathematics - or notations derived from mathematics. For example, in English we can say things like:
'I saw a man on a hill with a telescope.'
Who has the telescope? And then there is:
'Time flies like an arrow, fruit flies like a banana.'
You can do suprisingly well with natural language (and tables, diagrams etc.) - but for some applications it is not precise enough. Consider an analogy in the early history of programming languages. Most modern programming languages have a syntax defined using Backus Naur Form (BNF) - formal grammar, essentially. The first language to do this was Algol 60 (an early ancestor of the Pascal family of languages), and it was not initially popular. However it helped languages avoid syntactic anomolies. For example, this is a (legal) FORTRAN 'for' loop statement:
DO, 17 I = 1 10
However, if the ',' is left out, we get
DO 17 I = 1 10
which, because whitespace is not significant, FORTRAN cannot tell apart from the assignment statement
DO17I = 110
You do not have to declare variables in FORTRAN (which does not help), and DO17I is assumed to be floating-point because of the letter it begins with. (Hence the [slightly blasphemous] FORTRAN joke: 'God is real unless declared integer.')
This statement is 'famous' because it is often said that it caused the failure of a NASA interplanetary probe in the early 1960s. It's a nice story, but unfortunately it turns out to be false (though it is still often repeated). There was such a bug, but it was either fixed or not relevant and the probe was lost for other reasons.
Here is another example, from C (a language which post-dates BNF and has no excuse - though I suspect given its origins, BNF was not initially used for the syntax):
a = b / *c;
Hopefully, you have some idea of what this is supposed to do. However, if you leave out one space, you get:
a = b /*c;
and '/*' starts a comment, which means the statement does not compile because of the missing ';'. (If you are unlucky, you have a compiler clever enough to put it back in, and you don't notice the warning in with all the others.)
In the next chapter, we will revise some algebra, and introduce the idea of axioms.