|
High Integrity Software: The SPARK Approach to safety & Secrity
1. Introduction.
Software and its problems.
Correctness by construction.
Rationale for Spark.
Spark language features.
Tool support.
Examples.
Historical note.
Structure of this book.
2. Language Principles.
Decomposition and abstraction.
Language support for abstraction.
Program
units.
Declarations and objects.
Subprograms.
Abstract data types.
Type extension.
Abstract state machines.
Refinement.
Program composition.
3. Spark Analysis Tools.
Program correctness.
The Examiner.
Path functions.
Verification conditions.
Iterative processes.
Nested processes.
II. THE SPARK LANGUAGE.
4. Spark Structure.
The definition of Spark.
Program units.
Lexical elements.
Pragmas.
5. The Type Model.
Objects.
Types and subtypes.
Enumeration types.
Numeric types.
Composite types.
Aggregates.
Names.
Expressions.
Constant and static expressions.
6. Control and Data Flow.
Statements.
Assignment statements.
Control statements.
Return statements.
Subprograms.
Primitive operations.
Procedure and function annotations.
Subprogram bodies and calls.
7. Packages and Visibility.
Packages.
Inherit clauses.
Own variables.
Package initialization.
Global definitions.
Private types.
Visibility.
Renaming.
Compilation units.
Subunits.
Compilation order.
8. Interfacing.
Interfacing pragmas.
Hidden text.
External variables.
The predefined library.
Spark_IO.
Implementation of Spark_IO.
Example of Spark_IO.
Interfacing to C.
Representation issues.
III. THE SPARK TOOLS.
9. The Spark Examiner.
Examination order.
Messages.
Option control.
Metafiles and index files.
Example of report file.
Proof options.
Other facilities.
10. Flow Analysis.
Production of verification conditions.
Control flow composition.
Information flow relations.
Sequences of statements.
Undefined variables.
Subprogram calls.
Conditional statements.
Loop statements and stability.
11. Verification.
Testing and verification.
Tool organization.
Run-time checks.
Functions and return annotations.
Proof contexts.
Proof functions.
Proof declarations and rules.
The FDL language.
Quantification.
Refinement and inheritance.
The Proof Checker.
12. Design Issues.
Some principles.
Architecture & Informed.
Location of state.
Package hierarchy.
Refinement and initialization of state.
Decoupling of state.
Boundary layer packages.
Summary of design guidelines.
Coding style.
13. Techniques.
Shadows.
Testing with children.
Unchecked conversion.
The Valid attribute.
Testpoints.
Memory-mapped constants.
Proof techniques.
14. Case Studies.
A lift controller.
Lift controller main program.
An autopilot.
Autopilot main program.
Altitude and heading controllers.
Run-time checks and the autopilot.
A sorting algorithm.
Proof of sorting algorithm.
Industrial applications.
APPENDICES.
A. Syntax.
Syntax of core Spark language.
Syntax of proof contexts.
B. Words, Attributes and Characters.
Spark words.
FDL words.
Attributes.
Character names.
C. Using the CD.
D. Work in Progress.
Answers to Exercises.
Bibliography.
Index. 0321136160T03072003
Copyright 2002 AW Higher Education Group, a division of Pearson Education, a Pearson plc company. All rights reserved. Legal disclaimer. E-mail webmaster@awl.com
|
