Programming languages and software engineering - The Computing Universe: A Journey through a Revolution - page 79

the computing arena. Universities were therefore able to order the data
tapes from Bell Labs for a nominal charge of $150 for materials. For that
they received the entire source code for the first general-purpose operat-
ing system for minicomputers. This along with the portable C compiler
was all that university researchers needed to produce their own ver-
sions. After July 1974, when a written version of their work appeared in
Communications of the ACM , orders came flooding in and first hundreds,
and then thousands of minicomputer users started porting Unix to their
machines. Thompson spent a sabbatical year in Berkeley in 1975 and
a graduate student named Bill Joy became an enthusiastic promoter of
Unix. By the early 1980s, the Berkeley System Distribution 4.2 Unix was
the de facto standard in the university research community. Joy and his
team were then commissioned by ARPA, the Advanced Research Projects
Agency, to integrate the newly defined networking protocol TCP/IP into
Unix. This was a very significant development for the birth of the Internet
as we shall see in Chapter 10 .

Fig. 4.13. The first edition of Kernighan
and Ritchie's C programming language
topic.

Formal methods

Software engineering involves many disciplines, including mathematics. In the context of software
development the field of formal methods uses a variety of mathematical techniques to specify and verify soft-
ware ( B.4.13 ). A formal specification of the system can be used to prove that the program has the desired
properties. Automated theorem proving systems attempt to prove that the software does what it was intended
to do by using its formal specification, a set of logical axioms and a set of inference rules to produce a formal
mathematical proof. An alternative approach uses model checking , which verifies properties of the system by
an exhaustive search of all the possible states that the system could enter during its execution. It is probably
fair to say that formal methods have not so far delivered major benefits for assisting the creation of bug-free
code in large software systems. However, there are now some examples of such methods being used to solve
real software problems. In 2002 Bill Gates said:

Things like even software verification, this has been the Holy Grail of computer science for many decades
but now in some very key areas, for example, driver verification we're building tools that can do actual proof
about the software and how it works in order to guarantee the reliability. 28

Gates was referring to the SLAM verification engine that checks that soft-
ware correctly satisfies the behavioral properties of the interfaces that it
uses. The SLAM tool is now applied regularly to all Microsoft device drivers
and has helped find more than three hundred bugs in the sample drivers
that were supplied to developers.

Databases

The main purpose of databases is to store and manage large
volumes of data. Database software plays a vital role in our modern
society. No bank transactions, online shopping, airline reservations,
or even a checking out at the local supermarket would be possible
without databases. Database software is now a multibillion dollar
business.

B.4.13. Three pioneers of structured
programming and formal methods in
software development: Tony Hoare,
Edsger Dijkstra, and Niklaus Wirth seen
here at an Alpine resort.