Overview
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.