- ホーム
- > 洋書
- > 英文書
- > Computer / General
Full Description
This book provides an accessible introduction to the SPARK programming language.* Updated 'classic' that covers all of the new features of SPARK, including Object Oriented Programming. * The only book on the market that covers this important and robust programming language. * CD-ROM contains the main SPARK tools and additional manuals giving all the information needed to use SPARK in practice.Technology: The SPARK language is aimed at writing reliable software that combines simplicity and rigour within a practical framework. Because of this, many safety-critical, high integrity systems are developed using SPARK. User Level: Intermediate Audience: Software engineers, programmers, technical leaders, software managers. Engineering companies in fields such as avionics, railroads, medical instrumentation and automobiles. Academics giving MSc courses in Safety Critical Systems Engineering, System Safety Engineering, Software Engineering. Author Biography: 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
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
