High Integrity Software

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.

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