ANN: SPARK Proof - Tutorials and Tools

[JP Thornley <jpt@diphi.demon.co.uk>]

I have put a couple of tutorials on SPARK proof onto www.sparksure.com; 
one for proof of absence of run-time error (ie using the optional proof 
annotations) and one for using the Proof Checker. Both tutorials contain 
several sections, with worked examples and exercises.

I have also updated a couple of tools that help with SPARK proof:
1) VC_View makes it easier to read and interpret SPARK verification 
conditions.
2) PCHIF is an interface to the Proof Checker that makes it easier to 
recall and edit previously entered commands and to control the commands 
that are saved.
(Previous versions of PCHIF were very unstable, but this is now sorted, 
thanks to Dmitry Kazakov and Maxim Reznik for their Gtk Router.)

The tutorials and the tools (Windows executables only at present) can be 
downloaded from www.sparksure.com.

Phil Thornley
phil at sparksure dot com
-- 
JP Thornley