Barnes:High Integrity Ada_c

About

Features

Description

High Integrity Ada is an introduction to the SPARK programming language and its associated tools. Developed for the writing of high integrity software, SPARK is valued in application areas where getting the program right really matters.In John Barnesß clear and accessible writing style, this book combines a thorough description of the language with practical advice on how to use the SPARK tools. Illustrated with numerous examples and case studies, this book will teach you how to write more reliable software.The CD-ROM accompanying the book contains the SPARK tools plus additional documentation as well as all major examples of programs from the text.ß”he reader will enjoy John Barnesß lively guidance through SPARK. With panache he combines rigorous clarity and a great sense of fun.ߦrom the foreword by Bernard Carré߉߶e long watched for an approachable discussion of SPARK. This is it. ... The community and SPARK have long deserved to meet each other on such friendly terms.ߊames Sutton, Lockheedß”his book will be indispensable to the serious SPARK user, since it includes a very accessible definition of the language and provides all the necessary background material on static analysis as performed by the tools.ߐhil Thornley, British Aerospace

Sample Content

Table of Contents

Introduction.


Language Principles.


SPARK Analysis Tools.


SPARK Structure.


The Type Model.


Control and Data Flow.


Packages and Visibility.


Interfacing.


The SPARK Examiner.


Flow Analysis.


Verification; Program Design.


Case Studies. 0201175177T04192001

Updates

Submit Errata