Software is pervasive in our lives. We are accustomed to dealing with the failures of much of that software - restarting an application is a very familiar solution. Such solutions are unacceptable when the software controls our cars, airplanes and medical devices or manages our private information. These applications must run without error. SPARK provides a means, based on mathematical proof, to guarantee that a program has no errors. SPARK is a formally defined programming language and a set of verification tools specifically designed to support the development of software used in high integrity applications. Using SPARK, developers can formally verify properties of their code such as information flow, freedom from runtime errors, functional correctness, security properties and safety properties. Written by two SPARK experts, this is the first introduction to the just-released 2014 version. It will help students and developers alike master the basic concepts for building systems with SPARK.

nexusstc/Building High Integrity Applications with SPARK/0e52fe928b931acedcbaab6bbc503212.pdf

lgli/9781107656840---0e52fe928b931acedcbaab6bbc503212.pdf

lgrsnf/9781107656840---0e52fe928b931acedcbaab6bbc503212.pdf

zlib/Computers/Programming/John W Mccormick/Building High Integrity Applications with SPARK_16464720.pdf

High integrity programming with SPARK

McCormick, John W., Chapin, Peter C.

United Kingdom and Ireland, United Kingdom

New York, NY, 2015

Cambridge, 2015

lg3037060

{"edition":"1","isbns":["1107040736","1107656842","1139629298","9781107040731","9781107656840","9781139629294"],"last_page":382,"publisher":"Cambridge University Press"}

Half title 2
Title 4
Copyright 5
Table of Contents 7
Preface 10
1 Introduction and Overview 19
1.1 Obtaining Software Quality 20
1.2 What Is SPARK? 31
1.3 SPARK Tools 34
1.4 SPARK Example 38
Summary 44
Exercises 45
2 The Basic SPARK Language 47
2.1 Control Structures 54
2.2 Subprograms 66
2.3 Data Types 74
2.4 Subprograms, More Options 118
Summary 130
Exercises 131
3 Programming in the Large 136
3.1 Definition Packages 138
3.2 Utility Packages 141
3.3 Type Packages 144
3.4 Variable Packages 159
3.5 Child Packages 167
3.6 Elaboration 177
Summary 180
Exercises 182
4 Dependency Contracts 186
4.1 Data Dependency Contracts 187
4.2 Flow Dependency Contracts 195
4.3 Managing State 204
4.4 Default Initialization 229
4.5 Synthesis of Dependency Contracts 235
Summary 239
Exercises 242
5 Mathematical Background 247
5.1 Propositional Logic 247
5.2 Logical Equivalence 258
5.3 Arguments and Inference 262
5.4 Predicate Logic 268
Summary 280
Exercises 281
6 Proof 289
6.1 Runtime Errors 289
6.2 Contracts 301
6.3 Assert and Assume 348
6.4 Loop Invariants 367
6.5 Loop Variants 382
6.6 Discriminants 389
6.7 Generics 401
6.8 Suppression of Checks 419
Summary 427
Exercises 431
7 Interfacing with SPARK 437
7.1 SPARK and Ada 437
7.2 SPARK and C 459
7.3 External Subsystems 473
Summary 494
Exercises 496
8 Software Engineering with SPARK 499
8.1 Conversion of SPARK 2005 499
8.2 Legacy Ada Software 509
8.3 Creating New Software 518
8.4 Proof and Testing 536
8.5 Case Study: Time Stamp Server 540
Summary 566
9 Advanced Techniques 568
9.1 Ghost Entities 568
9.2 Proof of Transitive Properties 575
9.3 Proof Debugging 584
9.4 SPARK Internals 604
Notes 614
References 620
Index 628

The formally defined programming language SPARK provides a means to guarantee that a computer program has no errors. This makes it a natural system for designing safety- and security-critical applications. This first introduction to SPARK 2014 will allow students and developers to master the basic concepts for building systems with SPARK.

2021-06-24