 |
"High Integrity Software: The SPARK Approach to Safety
and Security" by John Barnes
Tool Upgrades
Sample Chapters
Buying the Book
FAQ
Errata
Tool Support – Known Issues
Upgrading to the Professional Toolset
Tool Upgrades
New - 1st June 2007. Upgrade packages for
the demonstration tools for Release 7.5 of the SPARK Toolset
are now available.
Each of these packages includes new tools (Examiner 7.5, Simplifier
2.32, POGS 4.7, and SPARKFormat 7.5), plus the complete set
of documentation describing SPARK, RavenSPARK and the tools.
A Readme file is included in each describing the upgrade process.
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 packages without
having first read the book.
Windows – (8 Megabytes
ZIP file)
GNU/Linux – (7.7
Megabytes .tar.gz file)
Apple Mac PowerPC/OS
X – (7.2 Megabytes .tar.gz file)
Note - be sure to unpack the tarballs with the "p"
option (preserve file permissions) flag.
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.
The book is available for order in book stores.
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 – Known Issues
A small number of issues with the demonstration tools have
been brought to our attention since the CDROM was finalized
for production.
1. Process Limits (Linux) – The Examiner and POGS require
significant amounts of Stack memory. If you get a "segfault"
when running these tools, then you need to "unlimit"
your process's maximum stack size. The default limit on some
Linux distributions is 8 Megabytes – this is not sufficient
for POGS, which requires about 15 Megabytes. This issue is
corrected in versions of POGS greater than 3.1.
2. Spaces in Directory Names (Windows) – We recommend
that the tools are installed in a directory that doesn't have
any spaces in its path name, such as "C:\praxis"
rather than "C:\Program Files\praxis". We have had
a report that this causes problems for the Simplifier, but
we have not been able to reproduce this issue at present.
If you encounter any other 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 Toolset, then please contact
us at sparkinfo@praxis-his.com.
|
|
