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 is being actively used in industry (e.g., avionics), so it is of particular interest.
Here's an overview of the language and tools.
Posted to Software-Eng by Ehud Lamm on 3/12/03; 3:19:21 AM