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-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,9741d8c9cef792de
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2003-03-28 03:47:29 PST
Path: 
 archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news-spur1.maxwell.syr.edu!news.maxwell.syr.edu!newsfeed.icl.net!newsfeed.fjserv.net!newsfeed.icl.net!newsfeed.fjserv.net!news-FFM2.ecrc.net!news.iks-jena.de!not-for-mail
From: Lutz Donnerhacke <lutz@iks-jena.de>
Newsgroups: comp.lang.ada
Subject: Re: [Spark] Some Linux tools
Date: Fri, 28 Mar 2003 11:47:28 +0000 (UTC)
Organization: IKS GmbH Jena
Message-ID: <slrnb88die.oi.lutz@taranis.iks-jena.de>
References: <slrnb7mhmi.nu.lutz@taranis.iks-jena.de>
 <slrnb7u4b3.o1.lutz@taranis.iks-jena.de>
 <cf2c6063.0303271003.1bdac074@posting.google.com>
NNTP-Posting-Host: taranis.iks-jena.de
X-Trace: branwen.iks-jena.de 1048852048 26255 217.17.192.37 (28 Mar 2003
 11:47:28 GMT)
X-Complaints-To: usenet@iks-jena.de
NNTP-Posting-Date: Fri, 28 Mar 2003 11:47:28 +0000 (UTC)
User-Agent: slrn/0.9.7.4 (Linux)
Xref: archiver1.google.com comp.lang.ada:35784
Date: 2003-03-28T11:47:28+00:00
List-Id: <comp.lang.ada>

* Rod Chapman wrote:
> Thanks for posting those scripts - I'm sure many buyers of the SPARK
> book will find them useful.  Can you clarify two issues, though:
>  1) Who is the copyright holder for these scripts?

Lutz Donnerhacke, Jena, Thuringia, Germany, Europe, Earth, Solar System,
Milky Way, Local Group, ...

>  2) Under what licence terms are these scripts supplied?

Free licence: Take it at your own risk, modify it, keep the modifications
secret, sell them, ignore to mention me, ...

If someone provide me an example output of the Proof Checker logfile, I can
add this. Path functions are unsupported, because I do not need them.

(Larger programs are usually GP(L)Led.)

Recent modifications:
  - Computes hashs over VCs in order to check them against those mentioned in
    the Review Team logfile. This ensures, that modified VCs are not longer
    considered proofed by the review team.
  - Prints 'old' instead of 'yes' in the summary if the simplifier/checker
    result is older than the examiner output.

In order to considerably speed up the simplifier/checker process, it's worth
to check hashs over the examiner generated files. This may render several
simplifier/checker calls unnecessary due to unmodified preconditions.

I'll think about this.