Re: New SPARK book is published today

["G.B." <bauhaus@futureapps.invalid>]

On 03.09.15 12:08, Dirk Craeynest wrote:
> In article <db0417bf-0509-4a2a-a90f-fc6df66b6c56@googlegroups.com>,
> Vincent  <vincent.diemunsch@gmail.com> wrote:
> [...about the new SPARK book by John McCormick and Peter Chapin...]
>> That's interesting. Would it be possible to see the content of the book,
>> i.e. the name of the chapters ? I coudn't find the information on Amazon.
>
> Some information is available on the publisher's web-page for the book.
> See the tab "Contents" on:
>
> <http://www.cambridge.org/us/academic/subjects/computer-science/programming-languages-and-applied-logic/building-high-integrity-applications-spark>
>
> Dirk
>

A Kindle "sample" may now be received from Amazon; it includes
the Preface, with chapter outlines, and some of the introductory
chapter. Also included is this TOC:


Preface

1 Introduction and Overview

1.1 Obtaining Software Quality
1.2 What Is SPARK?
1.3 SPARK Tools
1.4 SPARK Example
Summary
Exercises

2 The Basic SPARK Language

2.1 Control Structures
2.2 Subprograms
2.3 Data Types
2.4 Subprograms, More Options
Summary
Exercises

3 Programming in the Large

3.1 Definition Packages
3.2 Utility Packages
3.3 Type Packages
3.4 Variable Packages
3.5 Child Packages
3.6 Elaboration
Summary
Exercises

4 Dependency Contracts

4.1 Data Dependency Contracts
4.2 Flow Dependency Contracts
4.3 Managing State
4.4 Default Initialization
4.5 Synthesis of Dependency Contracts
Summary
Exercises

5 Mathematical Background

5.1 Propositional Logic
5.2 Logical Equivalence
5.3 Arguments and Inference
5.4 Predicate Logic
Summary
Exercises

6 Proof

6.1 Runtime Errors
6.2 Contracts
6.3 Assert and Assume
6.4 Loop Invariants
6.5 Loop Variants
6.6 Discriminants
6.7 Generics
6.8 Suppression of Checks
Summary
Exercises

7 Interfacing with SPARK

7.1 SPARK and Ada
7.2 SPARK and C
7.3 External Subsystems
Summary
Exercises

8 Software Engineering with SPARK

8.1 Conversion of SPARK 2005
8.2 Legacy Ada Software
8.3 Creating New Software
8.4 Proof and Testing
8.5 Case Study: Time Stamp Server
Summary

9 Advanced Techniques

9.1 Ghost Entities
9.2 Proof of Transitive Properties
9.3 Proof Debugging
9.4 SPARK Internals

Notes
References
Index