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=0.5 required=5.0 tests=BAYES_00,TO_NO_BRKTS_PCNT, T_FILL_THIS_FORM_SHORT autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,ff699839add5f2cd,start X-Google-Attributes: gid103376,public X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news4.google.com!newsfeed2.dallas1.level3.net!news.level3.com!newsfeed-00.mathworks.com!news.tele.dk!news.tele.dk!small.news.tele.dk!newsfeed00.sul.t-online.de!newsfeed01.sul.t-online.de!t-online.de!newsfeed.vmunix.org!peer-uk.news.demon.net!kibo.news.demon.net!news.demon.co.uk!demon!diphi.demon.co.uk!jpt From: JP Thornley Newsgroups: comp.lang.ada Subject: A couple of tools for SPARK Proof Date: Mon, 6 Jun 2005 17:51:52 +0100 Message-ID: NNTP-Posting-Host: diphi.demon.co.uk Mime-Version: 1.0 Content-Type: text/plain;charset=us-ascii;format=flowed X-Trace: news.demon.co.uk 1118077054 13040 80.177.171.182 (6 Jun 2005 16:57:34 GMT) X-Complaints-To: abuse@demon.net NNTP-Posting-Date: Mon, 6 Jun 2005 16:57:34 +0000 (UTC) User-Agent: Turnpike/6.04-S () Xref: g2news1.google.com comp.lang.ada:11247 Date: 2005-06-06T17:51:52+01:00 List-Id: I've developed a couple of tools to help when doing Spark proof - called VC_View and PCHIF. The purpose of VC_View is to make it easier to read and interpret Spark VCs. It does this in two ways: 1. Only immediately relevant hypotheses are initially shown 2. User identifiers are replaced by upper case letters The hypotheses that are shown initially are those that share an identifier with a conclusion. These can then be selectively extended. Other features allow the hypotheses to be restricted to just those for a single conclusion, and give access to the rules file for the VCs. The main purposes of PCHIF are to make it easier to recall and edit previously entered commands and to give better control over the commands that are stored. As well as making it easier to create proof scripts, PCHIF should also simplify the creation of 'clean' scripts - i.e. ones without failed inferences, etc. (A long term ambition for PCHIF is to simplify the maintenance of proof scripts by providing a 'stop on fail' feature - to make it easier to pinpoint commands that need changing.) At present PCHIF is an experimental prototype and has a number of limitations - the main one is that it only handles input to the Checker. (In order to handle the output from the Checker it must be piped to another program - when this is done the Checker prompts don't appear down the pipe until after the Checker has received the input that it is prompting for.) Both tools are 100% Ada, and compiled with GNAT 3.15p. Only MS Windows executables are provided (XP Pro, but may work on other versions). However they use GtkAda so it should be possible to compile them for other platforms. (The sources aren't currently provided for download but I intend to make them available once they've been made fit for public view.) The download page can be reached from www.sparksure.com. If you try the tools, please use the contact email address given on the sparksure pages to send me comments. Cheers, Phil Thornley -- JP Thornley