New SPARK book is published today

New SPARK book is published today

[roderick.chapman]

Hi everyone,
 I'm pleased to say that the all-new SPARK book by John McCormick and
Peter Chapin is published today.  It covers the SPARK 2014 language and
tools in some detail.  Available for order on Amazon and all the usual
places now.  For example:

http://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107656842/ref=sr_1_1?ie=UTF8&qid=1441267363&sr=8-1&keywords=mccormick+chapin+spark

 - Rod

Re: New SPARK book is published today

[Vincent]

Le jeudi 3 septembre 2015 10:10:35 UTC+2, roderick...@googlemail.com a écrit :
> Hi everyone,
>  I'm pleased to say that the all-new SPARK book by John McCormick and
> Peter Chapin is published today.  It covers the SPARK 2014 language and
> tools in some detail.

Hello Rod,

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.

Regards,

Vincent

Re: New SPARK book is published today

[Dirk Craeynest]

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

Re: New SPARK book is published today

[G.B.]

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

Re: New SPARK book is published today

[Mark Lorenzen]

On Thursday, September 3, 2015 at 10:10:35 AM UTC+2, roderick...@googlemail.com wrote:
> Hi everyone,
>  I'm pleased to say that the all-new SPARK book by John McCormick and
> Peter Chapin is published today.  It covers the SPARK 2014 language and
> tools in some detail.  Available for order on Amazon and all the usual
> places now.  For example:
> 
> http://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107656842/ref=sr_1_1?ie=UTF8&qid=1441267363&sr=8-1&keywords=mccormick+chapin+spark

Excellent! I ordered a copy at Amazon UK yesterday.

Unfortunately the delivery time is estimated to be at least 14 days, but I guess that's the price to pay for ordering an all-new book.

Regards,

Mark L

Re: New SPARK book is published today

[Jerry van Dijk]

In article <de199bbb-2f55-4dbc-91f6-b168341596f3@googlegroups.com>, 
mark.lorenzen@gmail.com says...

> Unfortunately the delivery time is estimated to be at least 14 days, 
but I guess that's the price to pay for ordering an all-new book.

Ha! Thats at least one better than Amazon.com:

Delivery estimate: We need a little more time to provide you with a good 
estimate. We'll notify you via e-mail as soon as we have an estimated 
delivery date.

-- 
-- Jerry van Dijk
-- Leiden, Holland
--
-- Some say I'm a grumpy 'ol wizzard, but that's not true.
-- I have the heart of a kind and gentle soul... in a jar, on my desk.

Re: New SPARK book is published today

[Mark Lorenzen]

On Thursday, September 10, 2015 at 11:40:03 AM UTC+2, Jerry van Dijk wrote:
> 
> Ha! Thats at least one better than Amazon.com:
> 
> Delivery estimate: We need a little more time to provide you with a good 
> estimate. We'll notify you via e-mail as soon as we have an estimated 
> delivery date.
> 
> -- 
> -- Jerry van Dijk
> -- Leiden, Holland
> --
> -- Some say I'm a grumpy 'ol wizzard, but that's not true.
> -- I have the heart of a kind and gentle soul... in a jar, on my desk.

It seems to go fast now. My copy was dispatched from Amazon UK on Friday, so order away folks!

Regards,

Mark L