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,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,48e1a3c594fb62e8 X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!postnews.google.com!p2g2000yqh.googlegroups.com!not-for-mail From: Rod Chapman Newsgroups: comp.lang.ada Subject: Re: SPARK Date: Fri, 14 May 2010 02:32:05 -0700 (PDT) Organization: http://groups.google.com Message-ID: <1fa6a7b3-ae22-4223-bd11-bbf2dff411c7@p2g2000yqh.googlegroups.com> References: <30e0a8bd-e6f8-425c-9423-6eba7f35972d@n15g2000yqf.googlegroups.com> NNTP-Posting-Host: 88.128.92.147 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 X-Trace: posting.google.com 1273829526 19196 127.0.0.1 (14 May 2010 09:32:06 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Fri, 14 May 2010 09:32:06 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: p2g2000yqh.googlegroups.com; posting-host=88.128.92.147; posting-account=HCzrEgkAAABSfGsTnv-u5wET6EzuneVi User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-GB; rv:1.9.1.9) Gecko/20100315 Firefox/3.5.9 (.NET CLR 3.5.30729),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:11600 Date: 2010-05-14T02:32:05-07:00 List-Id: > As you are discovering, the documentation for the optional proof > assertions in SPARK is not easy to find (it is spread across several > documents, and rather scattered within those documents). Noted. For SPARK Pro 9.0, we merged all the Proof material into one manual and gave it the rather more obvious title "Proof Manual". We also produced a one-page clickable index to _all_ the manuals, which has also proven useful. - Rod Chapman, SPARK Team