From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,121ed47e1e990d4d,start X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news3.google.com!news.germany.com!news.k-dsl.de!border-3.ams.xsnews.nl!feed.xsnews.nl!border-4.ams.xsnews.nl!69.16.177.242.MISMATCH!cyclone02.ams2.highwinds-media.com!news.highwinds-media.com!npeersf02.ams.highwinds-media.com!newsfe21.ams2.POSTED!7564ea0f!not-for-mail Message-ID: From: JP Thornley Newsgroups: comp.lang.ada Subject: ANN: SPARK Proof - Tutorials and Tools MIME-Version: 1.0 Content-Type: text/plain;charset=us-ascii;format=flowed User-Agent: Turnpike/6.07-S (<10xliejdassucTFOrzXcAbnrrC>) NNTP-Posting-Host: 80.177.171.182 X-Complaints-To: abuse@demon.net X-Trace: newsfe21.ams2 1237464962 80.177.171.182 (Thu, 19 Mar 2009 12:16:02 UTC) NNTP-Posting-Date: Thu, 19 Mar 2009 12:16:02 UTC Date: Thu, 19 Mar 2009 12:13:57 +0000 Xref: g2news1.google.com comp.lang.ada:4187 Date: 2009-03-19T12:13:57+00:00 List-Id: 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