 |
"High Integrity Software: The SPARK Approach to Safety
and Security" by John Barnes
Tool Downloads and Upgrades
Sample Chapters
Buying the Book
Errata
Tool Support – Known Issues
Upgrading to the Professional Toolset
Tool Downloads and Upgrades
Downloaded Tokeneer? Need the SPARK Toolset?
You have two options - academic faculty should
get the full SPARK toolset via AdaCore's
GAP programme.
Everyone else can download the SPARK GPL
Edition from the Libre
Website.
These packages are designed for use by those that have studied
the book and have an understanding of the concepts described.
We do not recommend that you attempt to use the SPARK Toolset
without having first read the book.
Note: the new SPARK GPL Edition toolset completely replaces
and supersedes the earlier "demo" versions of the
toolset that were supplied with the book.
Sample Chapters
The Sample Chapters are
now available in PDF (612k).
Buying the Book
The book is available for order on various websites, including
amazon.com,
Barnes
and Noble, and amazon.co.uk.
October 2008: The book is now undergoing
a 4th re-print, so please be patient if booksellers appear
to be out of stock.
The book is published by Addison Wesley. Their page is here.
The ISBN Number is 0-321-13616-0.
Errata (for the first print)
We'd like to hear from you if you think you've found a mistake
in the book! We currently know of seven (small) issues:
1. On p. 336, two semi-colons are missing: in procedure Zero_Totals,
and at the end of procedure Add.
2. On p. 337, a semi-colon is missing from the end of the
inherit annotation of package Convert.
3. On p. 338, a semi-colon is missing from the end of the
inherit annotation of package Convert. (Cut and Paste error!)
4. On p. 339, the assignment statement to "Local"
ends in a colon. This should, of course, be a semi-colon.
5. On p. 365, the heading and first paragraph of section 14.6
is typeset too wide. (It should be the same width as the reset
of the main body text.)
6. On p. 422, second line – Andy's surname is spelt incorrectly.
It should be "Pryor", not "Prior".
7. On p. 89, the assignment statement in the body of procedure
Check is wrong. It should read "B := F > Start and
F < Stop;"
Tool Support
If you encounter any issues, please contact us at sparkinfo@praxis-his.com.
Upgrading to the Professional Toolset
If you're interested in obtaining the full, professionally
supported version of the SPARK Pro Toolset, then please contact
us via sales@adacore.com
|
|
