High Integrity Software, w. CD-ROM

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

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.