Computer Science

• Updated 'classic' that covers all of the new features of SPARK, including Object Oriented Programming.
• CD-ROM contains the main SPARK tools and additional manuals giving all the information needed to use SPARK in practice.

Contents
Foreword
Preface
PART 1 AN OVERVIEW
1 Introduction
1.1 Software And Its Problems
1.2 Correctness By Construction
1.3 Rationale For SPARK
1.4 SPARK Language Features
1.5 Tool Support
1.6 Examples
1.7 Historical Note
1.8 Structure Of This Book
2 Language Principles
2.1 Decomposition And Abstraction
2.2 Language Support For Abstraction
2.3 Program Units
2.4 Declarations And Objects
2.5 Subprograms
2.6 Abstract Data Types
2.7 Type Extension
2.8 Abstract State Machines
2.9 Refinement
2.10 Program Composition
3 SPARK Analysis Tools
3.1 Program Correctness
3.2 The Examiner
3.3 Path Functions
3.4 Verification Conditions
3.5 Iterative Processes
3.6 Nested Processes
PART 2 THE SPARK LANGUAGE
4 SPARK Structure
4.1 The Definition Of SPARK
4.2 Program Units
4.3 Lexical Elements
4.4 Pragmas
5 The Type Model
5.1 Objects
5.2 Types And Subtypes
5.3 Enumeration Types
5.4 Numeric Types
5.5 Composite Types
5.6 Aggregates
5.7 Names
5.8 Expressions
5.9 Constant And Static Expressions
6 Control And Data Flow
6.1 Statements
6.2 Assignment Statements
6.3 Control Statements
6.4 Return Statements
6.5 Subprograms
6.6 Primitive Operations
6.7 Procedure And Function Annotations
6.8 Subprogram Bodies And Calls
7 Packages And Visibility
7.1 Packages
7.2 Inherit Clauses
7.3 Own Variables
7.4 Package Initialization
7.5 Global Definitions
7.6 Private Types
7.7 Visibility
7.8 Renaming
7.9 Compilation Units
7.10 Subunits
7.11 Compilation Order
8 Interfacing
8.1 Interfacing Pragmas
8.2 Hidden Text
8.3 External Variables
8.4 The Predefined Library
8.5 Spark_IO
8.6 Implementation Of Spark_IO
8.7 Example Of Spark_IO
8.8 Interfacing To C
8.9 Representation Issues
PART 3 THE SPARK TOOLS
9 The SPARK Examiner
9.1 Examination Order
9.2 Messages
9.3 Option Control
9.4 Metafiles And Index Files
9.5 Example Of Report File
9.6 Proof Options
9.7 Other Facilities
10 Flow Analysis
10.1 Production Of Verification Conditions
10.2 Control Flow Composition
10.3 Information Flow Relations
10.4 Sequences Of Statements
10.5 Undefined Variables
10.6 Subprogram Calls
10.7 Conditional Statements
10.8 Loop Statements And Stability
11 Verification
11.1 Testing And Verification
11.2 Tool Organization
11.3 Run-Time Checks
11.4 Functions And Return Annotations
11.5 Proof Contexts
11.6 Proof Functions
11.7 Proof Declarations And Rules
11.8 The FDL Language
11.9 Quantification
11.10 Refinement And Inheritance
11.11 The Proof Checker
12 Design Issues
12.1 Some Principles
12.2 Architecture & INFORMED
12.3 Location Of State
12.4 Package Hierarchy
12.5 Refinement And Initialization Of State
12.6 Decoupling Of State
12.7 Boundary Layer Packages
12.8 Summary Of Design Guidelines
12.9 Coding Style
13 Techniques
13.1 Shadows
13.2 Testing With Children
13.3 Unchecked Conversion
13.4 The Valid Attribute
13.5 Testpoints
13.6 Memory-Mapped Constants
13.7 Proof Techniques
14 Case Studies
14.1 A Lift Controller
14.2 Lift Controller Main Program
14.3 An Autopilot
14.4 Autopilot Main Program
14.5 Altitude And Heading Controllers
14.6 Run-Time Checks And The Autopilot
14.7 A Sorting Algorithm
14.8 Proof Of Sorting Algorithm
14.9 Industrial Applications
Appendices
A1 Syntax
A1.1 Syntax Of Core SPARK Language
A1.2 Syntax Of Proof Contexts
A2 Words, Attributes And Characters
A2.1 SPARK Words
A2.2 FDL Words
A2.3 Attributes
A2.4 Character Names
A3 Using The CD
A4 Work In Progress
Answers To Exercises
Bibliography
Index

Ada--Data Structures  [PTG: NEW RIDERS]   (Computer Science)

John Barnes is a veteran of the computing industry.  In 1977 he designed and implemented the RTL/2 programming language and was an original member of the ADA programming language design team.  He was founder and MD of Alsys Ltd from 1985 to 1991.  Currently self employed, John is the author of 'Programming in ADA' which has sold 150000 copies and been translated into 6 languages.  

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

Pearson Higher Education offers special pricing when you choose to package your text with other student resources. If you're interested in creating a cost-saving package for your students contact your Pearson Higher Education representative.