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=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!news.glorb.com!Xl.tags.giganews.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Thu, 20 Aug 2015 13:42:11 -0500
Newsgroups: comp.lang.ada
Date: Thu, 20 Aug 2015 14:42:09 -0400
From: Peter Chapin <PChapin@vtc.vsc.edu>
X-X-Sender: pcc09070@WIL414CHAPIN.vtc.vsc.edu
Subject: Re: Problems with SPARK 2015 and XMLAda
In-Reply-To: <9d3dc132-4e1a-4e9c-bcd4-82a42a73745f@googlegroups.com>
Message-ID: <alpine.CYG.2.11.1508201440030.7892@WIL414CHAPIN.vtc.vsc.edu>
References: <e3de50ce-e994-4038-8160-13266aeb207e@googlegroups.com>
 <lymvxn112j.fsf@pushface.org>
 <6952b70d-a9bc-4d0a-beb5-1cd38d6a3318@googlegroups.com>
 <9d3dc132-4e1a-4e9c-bcd4-82a42a73745f@googlegroups.com>
User-Agent: Alpine 2.11 (CYG 23 2013-08-11)
Organization: Vermont Technical College
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
X-Usenet-Provider: http://www.giganews.com
X-Trace: 
 sv3-aZXbOXiKwUG6BB5Q3CoSjJFpivrOyLm0kI/j77XhCKux/pANsXq4M2R1WUZAibZ/TdxIaPWaoQ/A1F0!l9AEJGQysI8XqU568mWz4UUrQi/80RLwwgE0x3GAi/uNp6lg8QBQmA6+qcevb8n7Eh4PfsaZckBv!5MZgSm36T5fmipC37w==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint
 properly
X-Postfilter: 1.3.40
X-Original-Bytes: 2029
Xref: news.eternal-september.org comp.lang.ada:27531
Date: 2015-08-20T14:42:09-04:00
List-Id: <comp.lang.ada>

On Thu, 20 Aug 2015, Shark8 wrote:

> As others have said, SPARK is about avoiding exceptions completely 
> (because the relevant properties are proved) and therefore having 
> exceptions in your SPARK code is not allowed.

To clarify, SPARK 2014 does allow raise statements in programs. However, 
each Raise statement carries with it a proof obligation that it will never 
execute. What's the point of that? It allows you to use raise statements 
to document "impossible" situations and then have the tools attempt to 
prove that those situations are, indeed, impossible.

SPARK 2014 does not allow exception handlers, however.

Peter