This book is about programming in Spark--a language highly suited for writing programs that need to be reliable, and thus particularly relevant to those application areas where safety or security are important. It is a major revision of the previous book which was entitled High Integrity Ada.
Spark is sometimes regarded as being just a subset of Ada with various annotations that you have to write as Ada comments. This is mechanically correct but is not at all the proper view to take. Spark should be seen as a distinct language in its own right and that is one reason why the title was changed in this edition.
Spark has just those features required for writing reliable software: not so austere as to be a pain, but not so rich as to make program analysis out of the question. But it is sensible to share compiler technology with some other standard language and it so happens that Ada provides a better framework than many other languages. In fact, Ada seems to be the only language that has good lexical support for the concept of programming by contract by separating the ability to describe a software interface (the contract) from its implementation (the code) and enabling these to be analysed and compiled separately. The Eiffel language has created a strong interest in the concept of programming by contract which Spark has embodied since its inception in the late 1980s.
There has recently also been interest in reliable software in areas other than those that have traditionally cared about reliability (avionics and railroads). It is now beginning to be realized that reliable software matters in other areas, such as finance, communications, medicine and motor cars.
Accordingly, I have changed the presentation with the goal that no knowledge of Ada is required to understand the discussion. However, there are some remarks comparing Spark and Ada which will be helpful to those who do know Ada. Most of these are confined to the ends of sections and are in a different font but just a few are embedded in the text in square brackets. Either way they should not impede the discussion for the general reader.
I have always been interested in techniques for writing reliable software, if only (presumably like most programmers) because I would like my programs to work without spending ages debugging the wretched things.
Perhaps my first realization that the tools used really mattered came with my experience of using Algol 60 when I was a programmer in the chemical industry. It was a delight to use a compiler that stopped me violating the bounds of arrays; it seemed such an advance over Fortran and other even more primitive languages which allowed programs to violate themselves in an arbitrary manner.
On the other hand I have always been slightly doubtful of the practicality of the formal theorists who like to define everything in some turgid specification language before contemplating the process known as programming. It has always seemed to me that formal specifications were pretty obscure to all but a few and might perhaps even make a program less reliable in a global sense by increasing the problem of communication between client and programmer.
Nevertheless, I have often felt that underlying mathematical foundations can provide us with better tools even if the mathematical nature is somewhat hidden by a more practical facade. For example, enumeration types are really about sets but a deep understanding of set theory is not necessary in order to obtain the benefits of strong typing by realizing that a set of apples is not the same as a set of oranges.
Spark has this flavour of practical helpfulness underpinned by solid mathematical foundations. You don't have to understand the theorems of Boehm and Jacopini in order to obtain the benefits of good flow structure. Equally, Spark does not require esoteric annotations of a formal kind but quite simple affirmations of access and visibility which enable the Spark Examiner to effectively 'look over your shoulder' and identify inconsistencies between what you said you were going to do in the annotations and what you actually did in the code.
One of the advantages of Spark is that it may be used at various levels. At the simplest level of data flow analysis, the annotations ensure that problems of mistaken identity do not arise, that undefined values are not used and other similar flow errors are trapped. The next level of information flow analysis gives additional assurance regarding the inter-dependence between variables and can highlight unexpected relationships indicative of poorly organized data.For certain applications, formal proof may be useful and Spark provides a third level in which formal preconditions, postconditions and other assertions enable proofs to be established with the aid of the Spark tools.
However, formal proof is easily oversold; the effort involved in developing a proof can be high and in many cases might well be spent more effectively on other aspects of ensuring that a program is fit for its purpose. So the ability to apply Spark at various levels according to the application is extremely valuable.
A simple use of proof is in showing that a program is free from exceptions due to run-time errors such as those caused by overflow or writing outside an array. This can be done in a straightforward manner and does not require the addition of the more detailed annotations required for proof in general.
The various levels of analysis might even be mixed in a single program. The fine detail of key algorithms might be formally proved, higher organizational parts might benefit from information flow analysis, whereas the overall driving routines could well need only data flow analysis. And proof of freedom from run-time errors might be applied to the whole program.
I must say a little about the background to this book. I first encountered the foundation work done by Bob Phillips at Malvern when a consultant to the British Government and tasked with monitoring the usefulness of various research activities. I remember feeling that the flow analysis he was investigating was potentially good stuff but needed practical user interfaces.
That was twenty-five years ago. The current language and tools reflect the enormous energy put into the topic since then by Bernard Carre and his colleagues, first at Southampton University, then at Program Validation Limited and later at Praxis Critical Systems. The original approach was for the analysis of existing programs but now the emphasis is much more on writing the programs correctly in the first place.
However, it always seemed to me that although the tools and techniques were gaining steady acceptance, nevertheless both the tools and indeed the world of programmers deserved a more accessible description than that found in conference papers and user manuals.
A big impetus to actually do something was when my daughter Janet and I were invited by Program Validation Limited to join in a review of the formal definition of Spark and its further development. This resulted in a report familiarly known as Janet and John go a-Sparking (non-British readers should note that there is a series of children's books concerning the activities of Janet and John). Being involved in the review strengthened my feeling that a book would be very appropriate and, thanks to the support of Praxis, led to the first version of this book in 1997.
Since then, Spark and its tools have evolved further to include the safe parts of object oriented programming, a better means of interfacing to other parts of a system, a simpler means of showing that a program is free from exceptions, and more auditable means of proving that a program is correct. The various tools are also greatly improved both in terms of speed and quality of reporting.
These improvements justified this new book and I am most grateful for the support of Praxis in enabling me to write it. The CD at the back includes the latest demonstration versions of the major tools and electronic copies of a great deal of further documentation as well as the exercises and answers.The external reviewers included Kung-Kiu Lau, George Romanski, Jim Sutton, Tucker Taft and Phil Thornley; their comments were extremely valuable in ensuring that the book met its main objectives. I was greatly assisted by a number of staff of Praxis Critical Systems and I am especially grateful to Peter Amey, Rod Chapman, Jonathan Hammond and Adrian Hilton for their detailed comments and encouragement.
I must also continue to thank Bernard Carre for his vision in getting it all going; Bernard has now retired to warmer climes but his good work lives on.Finally, many thanks to my wife Barbara for her help in typesetting and proofreading, to friends at Addison-Wesley for their continued guidance and to Sheila Chatten for her help in the final stages of production.
"This book is indispensable to the serious SPARK user, giving a complete description of the enhanced SPARK language and analysis capabilities."
--Phil Thornley, Specialist in Safety Critical Software, BAE Systems.
"The SPARK approach provides a means by which good software engineering can bepracticed and be seen to be practiced. The book provides a rich description ofand rationale for the language, and could form the foundation for guidelinesused in the programming and verification of safety critical systems."
--George Romanski, President, Verocel Inc.
"John Barnes has used his characteristic witty style to provide the reader with all they need to understand and to start using the elegant features of the SPARK high integrity language and toolset."
--S. Tucker Taft, President, SofCheck Inc., and lead designer of Ada 95.
Our lives depend -- quite literally -- on software. Banking, transport, medical and industrial control systems rely on software to function correctly. In a software-powered world it is vital for our systems to be secure, reliable and safe.
The SPARK language and tools are designed to support the construction of "high integrity" systems, where safety and security are paramount. SPARK has been applied successfully in diverse applications including railway signalling, smartcard security and avionics systems in the Lockheed C130J and EuroFighter "Typhoon" projects.
The CD-ROM accompanying the book contains
- a demonstration version of the SPARK toolset and its documentation
- code examples from the text of the book
- Aonix ObjectAda compiler Special Edition
- GNAT Compiler public edition
John Barnes, in his clear and urbane style, combines a full description of SPARK with practical advice on using the SPARK tools. Numerous examples and case studies show readers how they can create more reliable software.